Well Typed Policies preserves is Authorized

theorem wellTypedPolicies_preserves_isAuthorized  {Γ : TypeEnv} {entities : Entities} {request : Request}  {ps ps' : Policies}  (hinst : InstanceOfWellFormedEnvironment request entities Γ)  (hwt : wellTypedPolicies ps Γ = .ok ps') :  isAuthorized request entities ps  = isAuthorized request entities ps':= by  have hpermit := wellTypedPolicies_preserves_satisfiedPolicies .permit hinst hwt  have hforbid := wellTypedPolicies_preserves_satisfiedPolicies .forbid hinst hwt  have herror := wellTypedPolicies_preserves_errorPolicies hinst hwt  simp only [Spec.isAuthorized, hpermit, hforbid, herror]