Partial authorize satisfied forbid is determining

theorem partial_authorize_satisfied_forbid_is_determining  {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 () →  response.satisfiedForbids ⊆ (Spec.isAuthorized req es policies).determiningPolicies:= by  intro h₁ h₂  simp only [TPE.isAuthorized] at h₁  cases h₃ : isAuthorized.evaluatePolicies schema policies preq pes <;>    simp [h₃] at h₁  subst h₁  have h_equiv := evaluatePolicies_residuals_equiv h₂ h₃  rename_i rps   simp only [isAuthorizedFromResiduals, isAuthorizedFromResiduals.satisfiedPolicies, Set.subset_def,    Set.mem_make, List.mem_filterMap, ResidualPolicy.satisfiedWithEffect,    ResidualPolicy.satisfied, Residual.isTrue, Bool.and_eq_true, beq_iff_eq,    Option.ite_none_right_eq_some, Option.some.injEq, forall_exists_index, and_imp]  intro pid rp hrp heff hs hpid  split at hs <;> try contradiction  rename_i hf₅   have ⟨p, hp₁, h_id, h_eff, h_eval⟩ := List.forall₂_implies_all_right h_equiv rp hrp   have ha : Spec.evaluate p.toExpr req es = .ok (.prim (.bool true)) := by    simp only [hf₅, Residual.evaluate] at h_eval    exact to_option_left_ok' h_eval   suffices h : pid ∈ satisfiedPolicies Effect.forbid policies req es by    have hd : IsExplicitlyForbidden req es policies := by      exists p; and_intros <;> grind [satisfied]    replace hd := forbid_trumps_permit _ _ _ hd    grind [Spec.isAuthorized]   simp only [satisfiedPolicies, satisfiedWithEffect, satisfied, Bool.and_eq_true, beq_iff_eq,    decide_eq_true_eq, Set.mem_make, List.mem_filterMap, Option.ite_none_right_eq_some,    Option.some.injEq]  exact ⟨p, hp₁, ⟨h_eff ▸ heff, ha⟩, h_id ▸ hpid⟩