Of Action Type ancs UDF is wf

theorem ofActionType_ancsUDF_is_wf  {uid : EntityUID} {Γ : TypeEnv}  {anc : EntityType}  {anc_f : UnaryFunction} (hwf : Γ.WellFormed)  (hanc :    (SymEntityData.ofActionType      uid.ty      (List.map (fun x => x.fst.ty) (Map.toList Γ.acts)).eraseDups      Γ.acts).ancestors.find? anc = some anc_f) :  UnaryFunction.WellFormed    (SymEnv.ofEnv Γ).entities    (SymEntityData.ofActionType.ancsUDF uid.ty Γ.acts anc) ∧  (SymEntityData.ofActionType.ancsUDF uid.ty Γ.acts anc).argType = .entity uid.ty ∧  (SymEntityData.ofActionType.ancsUDF uid.ty Γ.acts anc).outType = .set (.entity anc):= by  have hwf_acts := wf_env_implies_wf_acts_map hwf  simp only [    SymEntityData.ofActionType.ancsUDF,    UnaryFunction.argType,    UnaryFunction.outType,  ]  have := Map.find?_mem_toList hanc  simp only [Map.toList] at this  have := Map.mem_make_mem_list this  have ⟨anc_ty', hmem_anc', heq_anc'⟩ := List.mem_map.mp this  simp only [Prod.mk.injEq] at heq_anc'  simp only [heq_anc'.1] at hmem_anc'  and_intros  any_goals simp only  · constructor    · intros; contradiction    · intros; contradiction    · apply ofType_wf hwf      constructor      have := List.mem_eraseDups_implies_mem hmem_anc'      have ⟨act, hact, hact_ty⟩ := List.mem_map.mp this      apply Or.inr      simp only [        ActionSchema.IsActionEntityType,        ActionSchema.contains,      ]      have := (Map.in_list_iff_find?_some        (wf_env_implies_wf_acts_map hwf)).mp hact      exists act.fst      simp only [this, Option.isSome, true_and, hact_ty]    · simp [Set.empty, Set.WellFormed, Set.make, Set.toList, Set.elts, List.canonicalize]  · simp  · simp [TermType.ofType]  · simp only [Map.make_wf]  · -- WF of the ancestor UDF    intros tᵢ tₒ hmem    have := Map.mem_make_mem_list hmem    have ⟨act_entry, hact_entry, hsym⟩ := List.mem_filterMap.mp this    simp [bind, Option.bind] at hsym    split at hsym    contradiction    rename_i t₁ h₁    simp only [      SymEntityData.ofActionType.termOfType?,      Option.ite_none_right_eq_some,      Option.some.injEq,    ] at h₁    simp only [      Option.some.injEq, Prod.mk.injEq,      SymEntityData.ofActionType.ancsTerm,    ] at hsym    constructor    -- tᵢ is well-formed    · simp only [←hsym.1, ←h₁.2]      constructor      · constructor        constructor        have := (Map.in_list_iff_find?_some hwf_acts).mp hact_entry        have : Map.contains Γ.acts act_entry.fst := by          simp [Map.contains, this]        have := ofEnv_preserves_action_entity hwf this        simp only [          this,          SymEntities.isValidEntityUID,          SymEntityData.ofActionType,          SymEntityData.ofActionType.acts,          Set.contains,        ]        simp only [List.elem_eq_contains, List.contains_eq_mem, decide_eq_true_eq]        rw [Set.mem_elts_iff_mem_set, Set.mem_make]        apply List.mem_filterMap.mpr        exists act_entry        simp only [↓reduceIte, and_true]        apply (Map.in_list_iff_find?_some hwf_acts).mpr        assumption      · simp only [Term.isLiteral]    constructor    -- tᵢ has the right type    · simp [←h₁, ←hsym, typeOf_term_prim_entity, TermType.ofType]    -- tₒ is well-formed and has the right type    simp only [      ←hsym, TermType.ofType,      Term.WellFormedLiteral,    ]    apply and_assoc.mpr    apply and_left_comm.mp    constructor    · -- tₒ is literal      simp only [Factory.setOf]      apply lit_term_set_impliedBy_lit_elts      intros t hmem_t      rw [Set.mem_make] at hmem_t      have ⟨anc, hanc, hsym⟩ := List.mem_filterMap.mp hmem_t      simp only [        SymEntityData.ofActionType.termOfType?,        Option.ite_none_right_eq_some,        Option.some.injEq,      ] at hsym      simp only [←hsym, Term.isLiteral]    · apply wf_setOf      · intros t hmem_t        simp only [List.mem_filterMap] at hmem_t        have ⟨anc2, hmem_anc2, hsym⟩ := hmem_t        simp only [          SymEntityData.ofActionType.termOfType?,          Option.ite_none_right_eq_some,          Option.some.injEq,        ] at hsym        simp only [←hsym]        constructor        constructor        have := (Map.in_list_iff_find?_some hwf_acts).mp hact_entry        have ⟨anc_entry, hfind_anc_entry, hwf_anc_entry⟩ :=          wf_env_implies_wf_action_entity_ancestor hwf this hmem_anc2        have := ofEnv_preserves_action_entity hwf          (Map.find?_some_implies_contains hfind_anc_entry)        simp only [          SymEntities.isValidEntityUID,          this,          SymEntityData.ofActionType,          SymEntityData.ofActionType.acts,        ]        apply Set.contains_prop_bool_equiv.mpr        rw [Set.mem_make]        apply List.mem_filterMap.mpr        simp only [          Option.ite_none_right_eq_some,          Option.some.injEq, Prod.exists,          exists_and_right,        ]        exists anc2        simp only [and_self, and_true]        exists anc_entry        apply (Map.in_list_iff_find?_some hwf_acts).mpr        exact hfind_anc_entry      · intros t hmem_t        have ⟨anc, hanc, hsym⟩ := List.mem_filterMap.mp hmem_t        simp only [          SymEntityData.ofActionType.termOfType?,          Option.ite_none_right_eq_some,          Option.some.injEq,        ] at hsym        simp only [←hsym, typeOf_term_prim_entity]      · constructor        have := List.mem_eraseDups_implies_mem hmem_anc'        have ⟨_, h₁, h₂⟩ := List.mem_map.mp this        simp only [←h₂]        apply ofEnv_action_entity_exists hwf        simp [Map.contains, (Map.in_list_iff_find?_some hwf_acts).mp h₁]  · simp only [TermType.ofType]  · simp only [TermType.ofType]