Partial evaluate policy is sound

theorem partial_evaluate_policy_is_sound  {schema : Schema}  {residual : Residual}  {policy : Policy}  {req : Request}  {es : Entities}  {preq : PartialRequest}  {pes : PartialEntities}  {env : TypeEnv} :  evaluatePolicy schema policy preq pes = .ok residual →  schema.environment? preq.principal.ty preq.resource.ty preq.action = .some env →  InstanceOfWellFormedEnvironment req es env →  RequestAndEntitiesRefine req es preq pes →  (Spec.evaluate policy.toExpr req es).toOption = (Residual.evaluate residual req es).toOption:= by  intro h₁ h_schema_env h₄ h₃  simp [evaluatePolicy, h_schema_env] at h₁  split at h₁ <;> try cases h₁  cases hcheck : Except.mapError Error.invalidPolicy (checkEntities schema policy.toExpr) <;>    simp only [hcheck, Except.bind_err, reduceCtorEq] at h₁  simp [do_ok_eq_ok] at h₁  rcases h₁ with ⟨_, ⟨_, h₁₁⟩, h₁₂⟩  simp [Except.mapError] at h₁₁  split at h₁₁ <;> try cases h₁₁  rename_i ty _ _ heq₂  have h₅ := typechecked_is_well_typed_after_lifting heq₂  have h₉ : Residual.WellTyped env (TypedExpr.toResidual ty.liftBoolTypes) :=    conversion_preserves_typedness h₅  have h₆ := partial_evaluate_is_sound h₉ h₄ h₃  subst h₁₂  have h₇ := type_of_preserves_evaluation_results (empty_capabilities_invariant req es) h₄ heq₂  have h₈ : Spec.evaluate (substituteAction env.reqty.action policy.toExpr) req es = Spec.evaluate policy.toExpr req es := by    simp [InstanceOfWellFormedEnvironment] at h₄    rcases h₄ with ⟨_, h₄, _⟩    simp [InstanceOfRequestType] at h₄    rcases h₄ with ⟨_, h₄, _⟩    rw [←h₄]    exact substitute_action_preserves_evaluation policy.toExpr req es  simp [h₈] at h₇  rw [h₇, type_lifting_preserves_expr, ← h₆]  congr  apply conversion_preserves_evaluation