Denied iff explicitly denied or not permitted

theorem denied_iff_explicitly_denied_or_not_permitted (request: Request) (entities : Entities) (policies: Policies) :  (IsExplicitlyForbidden request entities policies ∨ ¬ IsExplicitlyPermitted request entities policies) ↔    (isAuthorized request entities policies).decision = .deny  := by  apply Iff.intro  · intro h    cases h    case inl => rw [forbid_trumps_permit]; assumption    case inr => rw [default_deny]; assumption  · intro h    by_cases h₁ : (IsExplicitlyForbidden request entities policies)    · exact Or.inl h₁    · right      rw [explicitly_forbidden_iff_satisfying_forbid] at h₁      rw [explicitly_permitted_iff_satisfying_permit]      unfold isAuthorized at h      simp [h₁] at h      split at h      · simp at h      · assumption