Of Type wf

theorem ofType_wf  {Γ : TypeEnv} {ty : CedarType}  (hwf : Γ.WellFormed)  (hwf_ty : CedarType.WellFormed Γ ty) :  (TermType.ofType ty).WellFormed (SymEnv.ofEnv Γ).entities:= by  cases ty with  | bool _ | int | string | ext _ => constructor  | entity ety =>    constructor    cases hwf_ty with | entity_wf hwf_ety =>    apply ofEnv_wf_entity hwf hwf_ety  | set sty =>    constructor    cases hwf_ty with | set_wf hwf_sty =>    exact ofType_wf hwf hwf_sty  | record rty =>    cases hwf_ty with | record_wf hwf_rty hwf_attrs =>    simp only [TermType.ofType, ofRecordType_eq_map]    constructor    · intros attr attr_ty hfind_attr      have := Map.find?_mem_toList hfind_attr      simp only [Map.toList_mk_id, List.mem_map, Prod.mk.injEq, Prod.exists] at this      replace ⟨a, qty, hmem, _, this⟩ := this ; subst a attr_ty      have hfind := hwf_attrs attr qty      have := (Map.in_list_iff_find?_some hwf_rty).mp hmem      specialize hfind this      cases hqty : qty with      | optional attr_ty' | required attr_ty' =>        simp only [hqty, TermType.ofQualifiedType] at hfind ⊢        cases hfind with | _ hfind =>        try constructor        exact ofType_wf hwf hfind    · apply Map.mapOnValues_wf.mp      exact hwf_rty