Substitute action preserves valid refs

theorem substitute_action_preserves_valid_refs  {Γ : TypeEnv} {request : Request} {entities : Entities} {expr : Expr}  (hinst : InstanceOfWellFormedEnvironment request entities Γ) :  entities.ValidRefsFor expr ↔ entities.ValidRefsFor (substituteAction request.action expr):= by  have ⟨hwf_Γ, _, ⟨_, hinst_sch⟩⟩ := hinst  have ⟨_, _, ⟨act_entry, hfind_act, _⟩⟩ := hwf_Γ  have heq_act : Γ.reqty.action = request.action := by    have ⟨_, ⟨_, h, _⟩, _⟩ := hinst    simp [h]  cases expr with  | lit p => simp only [substituteAction, mapOnVars]  | var v =>    simp only [substituteAction, mapOnVars]    split    · constructor      · intros        constructor        simp only [Prim.ValidRef]        simp only [heq_act] at hfind_act        have ⟨_, h⟩ := hinst_sch request.action act_entry hfind_act        simp only [Map.contains, h, Option.isSome]      · intros        constructor    · simp  | and e₁ e₂ | or e₁ e₂ | binaryApp _ e₁ e₂ =>    simp only [substituteAction, mapOnVars]    constructor    · intros hrefs      cases hrefs      rename_i hrefs₁ hrefs₂      constructor      · exact (substitute_action_preserves_valid_refs hinst).mp hrefs₁      · exact (substitute_action_preserves_valid_refs hinst).mp hrefs₂    · intros hrefs      cases hrefs      rename_i hrefs₁ hrefs₂      constructor      · exact (substitute_action_preserves_valid_refs hinst).mpr hrefs₁      · exact (substitute_action_preserves_valid_refs hinst).mpr hrefs₂  | ite e₁ e₂ e₃ =>    simp only [substituteAction, mapOnVars]    constructor    · intros hrefs      cases hrefs with | ite_valid hrefs₁ hrefs₂ hrefs₃ =>      constructor      · exact (substitute_action_preserves_valid_refs hinst).mp hrefs₁      · exact (substitute_action_preserves_valid_refs hinst).mp hrefs₂      · exact (substitute_action_preserves_valid_refs hinst).mp hrefs₃    · intros hrefs      cases hrefs with | ite_valid hrefs₁ hrefs₂ hrefs₃ =>      constructor      · exact (substitute_action_preserves_valid_refs hinst).mpr hrefs₁      · exact (substitute_action_preserves_valid_refs hinst).mpr hrefs₂      · exact (substitute_action_preserves_valid_refs hinst).mpr hrefs₃  | unaryApp _ e | getAttr e _ | hasAttr e _ =>    simp only [substituteAction, mapOnVars]    constructor    · intros hrefs      cases hrefs      rename_i hrefs      constructor      exact (substitute_action_preserves_valid_refs hinst).mp hrefs    · intros hrefs      cases hrefs      rename_i hrefs      constructor      exact (substitute_action_preserves_valid_refs hinst).mpr hrefs  | set s | call _ s =>    simp only [substituteAction, mapOnVars]    constructor    · intros hrefs      cases hrefs      rename_i hrefs      constructor      intros e' hmem_e'      have ⟨e, _, he'⟩ := List.mem_map.mp hmem_e'      have hmem_e := e.property      specialize hrefs e.val hmem_e      simp only [←he']      exact (substitute_action_preserves_valid_refs hinst).mp hrefs    · intros hrefs      cases hrefs      rename_i hrefs      constructor      intros e hmem_e      specialize hrefs (substituteAction request.action e)      apply (substitute_action_preserves_valid_refs hinst).mpr      apply hrefs      apply List.mem_map.mpr      exists ⟨e, hmem_e⟩      simp [substituteAction]  | record rec =>    simp only [substituteAction, mapOnVars]    constructor    · intros hrefs      cases hrefs      rename_i hrefs      constructor      intros attr_expr' hmem_attr_expr'      simp only [List.map₂_eq_map_snd] at hmem_attr_expr'      have ⟨attr_expr, hmem_attr_expr, hattr_expr⟩ := List.mem_map.mp hmem_attr_expr'      specialize hrefs attr_expr hmem_attr_expr      simp only [←hattr_expr]      exact (substitute_action_preserves_valid_refs hinst).mp hrefs    · intros hrefs      cases hrefs      rename_i hrefs      constructor      intros attr_expr hmem_attr_expr      specialize hrefs (attr_expr.fst, (substituteAction request.action attr_expr.snd))      apply (substitute_action_preserves_valid_refs hinst).mpr      apply hrefs      simp only [List.map₂_eq_map_snd]      apply List.mem_map.mpr      exists attr_expr