Of Env preserves action entity

theorem ofEnv_preserves_action_entity  {Γ : TypeEnv} {uid : EntityUID}  (hwf : Γ.WellFormed)  (hmem : Map.contains Γ.acts uid) :  Map.find? (SymEnv.ofEnv Γ).entities uid.ty =    some (SymEntityData.ofActionType      uid.ty      (Γ.acts.toList.map λ (act, _) => act.ty).eraseDups      Γ.acts):= by  simp only [SymEnv.ofEnv, SymEntities.ofSchema]  have hfind₁ :    (List.map      (fun x => (x.fst, SymEntityData.ofEntityType x.fst x.snd))      (Map.toList Γ.ets)    ).find? (λ ⟨k', _⟩ => k' == uid.ty) = none  := by    apply List.find?_eq_none.mpr    intros entry hmem_entry heq_ety_uid_ty    have ⟨ety, data⟩ := entry    have ⟨entry', hmem_entry', heq⟩ := List.mem_map.mp hmem_entry    have ⟨ety', data'⟩ := entry'    simp only [Prod.mk.injEq] at heq    have ⟨heq_ety, heq_data⟩ := heq    have hwf_ets : Map.WellFormed Γ.ets :=      wf_env_implies_wf_ets_map hwf    have hmem_ets := (Map.in_list_iff_find?_some hwf_ets).mp hmem_entry'    simp only [beq_iff_eq] at heq_ety_uid_ty    simp only [heq_ety, heq_ety_uid_ty] at hmem_ets    have ⟨_, hmem_acts⟩ := Map.contains_iff_some_find?.mp hmem    have := wf_env_disjoint_ets_acts hwf hmem_ets hmem_acts    contradiction  have hfind₂ :    ((List.map        (fun actTy =>          (actTy,            SymEntityData.ofActionType actTy              (List.map (fun x => x.fst.ty) (Map.toList Γ.acts)).eraseDups Γ.acts))        (List.map (fun x => x.fst.ty) (Map.toList Γ.acts)).eraseDups).find?      (λ ⟨k', _⟩ => k' == uid.ty)    ).isSome  := by    apply List.find?_isSome.mpr    simp only [      List.mem_map, beq_iff_eq, Prod.exists,      Prod.mk.injEq, exists_and_right,      exists_eq_right,    ]    apply Exists.intro    exists uid.ty    simp only [true_and]    constructor    · apply List.mem_implies_mem_eraseDups      apply List.mem_map.mpr      have ⟨entry, hmem_entry⟩ := Map.contains_iff_some_find?.mp hmem      exists (uid, entry)      simp only [and_true]      have hwf_acts : Map.WellFormed Γ.acts :=        wf_env_implies_wf_acts_map hwf      apply (Map.in_list_iff_find?_some hwf_acts).mpr      assumption    · rfl  have ⟨_, hfind, hmem⟩ := Map.map_make_append_find_disjoint hfind₁ hfind₂  simp only [hfind, Option.some.injEq]  have ⟨_, _, heq⟩ := List.mem_map.mp hmem  simp only [Prod.mk.injEq] at heq  have ⟨heq_uid_ty, heq⟩ := heq  simp only [heq_uid_ty] at heq  simp [heq]