Well Typed Policy preserves valid refs

theorem wellTypedPolicy_preserves_valid_refs  {Γ : TypeEnv} {request : Request} {entities : Entities} {p p' : Policy}  (hinst : InstanceOfWellFormedEnvironment request entities Γ)  (hwt : wellTypedPolicy p Γ = .ok p')  (hswf : entities.ValidRefsFor p.toExpr) :  entities.ValidRefsFor p'.toExpr:= by  have ⟨tx, tx', _, _, _, hty, heq_p', heq_tx'⟩ := wellTypedPolicy_ok_implies_exists_typed_exprs hwt  simp only [    heq_tx', TypedExpr.toExpr,    ←type_lifting_preserves_expr tx,  ] at heq_p'  simp only [heq_p']  repeat    constructor    repeat constructor  rotate_left  repeat constructor  apply typeOf_preserves_valid_refs entities hty  have : Γ.reqty.action = request.action := by    have ⟨_, ⟨_, h, _⟩, _⟩ := hinst    simp [h]  simp only [this]  apply (substitute_action_preserves_valid_refs hinst).mp  exact hswf