Partial authorize satisfied permits not determining if deny

theorem partial_authorize_satisfied_permits_not_determining_if_deny  {schema : Schema}  {policies : List Policy}  {req : Request}  {es : Entities}  {preq : PartialRequest}  {pes : PartialEntities}  {response : TPE.Response} :  TPE.isAuthorized schema policies preq pes = Except.ok response →  isValidAndConsistent schema req es preq pes = Except.ok () →  (Spec.isAuthorized req es policies).decision = .deny →  PolicyIdsUnique policies →  (response.satisfiedPermits ∩ (Spec.isAuthorized req es policies).determiningPolicies).isEmpty:= by  intro h₁ h₂ h₃ h₄  simp only [Set.empty_iff_not_exists, Set.mem_inter_iff, not_exists, not_and]  intro pid hp₁ hp₂   have hsatisfied : ∀ effect, (pid ∈ satisfiedPolicies effect policies req es ↔ (∃ policy, policy.id = pid ∧ policy ∈ policies ∧ policy.effect = effect ∧ satisfied policy req es)) := by    simp only [satisfiedPolicies, satisfiedWithEffect, Set.mem_make]    grind [PolicyIdsUnique]   replace hp₂ : ∃ policy, policy.id = pid ∧ policy ∈ policies ∧ policy.effect = .forbid ∧ satisfied policy req es := by    have hd := determiningPolicies_of req es policies    simpa [hd, h₃, hsatisfied] using hp₂   have hp₃ : ∃ policy, policy.id = pid ∧ policy ∈ policies ∧ policy.effect = .permit ∧ satisfied policy req es := by    have hpermits := partial_authorize_satisfied_permits_is_sound h₁ h₂    rw [Set.subset_def] at hpermits    rw [←hsatisfied]    exact hpermits pid hp₁   grind [PolicyIdsUnique]