Allowed iff explicitly permitted and not denied

theorem allowed_iff_explicitly_permitted_and_not_denied (request : Request) (entities : Entities) (policies : Policies) :  (IsExplicitlyPermitted request entities policies ∧ ¬ IsExplicitlyForbidden request entities policies) ↔  (isAuthorized request entities policies).decision = .allow:= by  apply Iff.intro  · intro ⟨h₁, h₂⟩    unfold isAuthorized    rw [explicitly_permitted_iff_satisfying_permit] at h₁    rw [explicitly_forbidden_iff_satisfying_forbid] at h₂    simp [h₁, h₂]  · intro h₁    have h₁' : ¬ (isAuthorized request entities policies).decision = Decision.deny := by simp [h₁]    have h₂ := (mt $ forbid_trumps_permit request entities policies) h₁'    have h₃ := allowed_only_if_explicitly_permitted request entities policies h₁    exact .intro h₃ h₂