Well Typed Policy preserves evaluation

theorem wellTypedPolicy_preserves_evaluation  {Γ : TypeEnv} {request : Request} {entities : Entities}  {p p' : Policy}  (hinst : InstanceOfWellFormedEnvironment request entities Γ)  (hwt : wellTypedPolicy p Γ = .ok p') :  evaluate p.toExpr request entities  = evaluate p'.toExpr request entities:= by  have ⟨tx, tx', _, hwt_tx_lift, hwt_tx', hty, heq_p'_tx', heq_tx', hbool⟩ := wellTypedPolicy_ok_implies_exists_typed_exprs hwt  have heq_action : Γ.reqty.action = request.action := by    have ⟨_, ⟨_, h, _⟩, _⟩ := hinst    simp [h]  have :    evaluate p.toExpr request entities    = evaluate (substituteAction Γ.reqty.action p.toExpr) request entities  := by    simp only [heq_action]    exact Eq.symm (substitute_action_preserves_evaluation _ _ _)  rw [this]  have heq :    evaluate (substituteAction Γ.reqty.action p.toExpr) request entities    = evaluate tx.toExpr request entities  := type_of_preserves_evaluation_results (empty_capabilities_invariant _ _) hinst hty  rw [heq]  simp only [    heq_p'_tx', heq_tx', TypedExpr.toExpr,    ←type_lifting_preserves_expr tx,  ]  simp only [    evaluate, Result.as,    Coe.coe, Value.asBool,    Bool.not_eq_eq_eq_not,    Bool.not_true, bind_pure_comp,    Functor.map, Except.map, Except.bind_ok,    Bool.true_eq_false,    ↓reduceIte,  ]  have ⟨_, ⟨v, heval, hwt_v⟩⟩ := type_of_is_sound (empty_capabilities_invariant _ _) hinst hty  simp only [EvaluatesTo, heq] at heval  rcases heval with heval | heval | heval | heval  · simp [heval]  · simp [heval]  · simp [heval]  . simp [heval]    simp only [type_of_after_lifted_is_lifted] at hbool    cases htx_ty : tx.typeOf with    | bool bt =>      simp only [htx_ty] at hwt_v      cases hwt_v with | instance_of_bool b bt hwt_v_bool =>      cases b <;> simp    | _ => simp [htx_ty, CedarType.liftBoolTypes] at hbool