Value symbolize? well typed

theorem value_symbolize?_well_typed  {Γ : TypeEnv} {v : Value} {ty : CedarType} {t : Term}  (hwf_ty : ty.WellFormed Γ)  (hwt_v : InstanceOfType Γ v ty)  (hsym : v.symbolize? ty = .some t) :  t.typeOf = TermType.ofType ty:= by  cases hwt_v with  | instance_of_bool | instance_of_int | instance_of_string =>    simp only [Value.symbolize?, Prim.symbolize, Option.some.injEq] at hsym    simp only [←hsym, typeOf_bool, typeOf_bv, typeOf_term_prim_string, TermType.ofType, Int64.toBitVec]  | instance_of_entity _ _ hwt_ety =>    simp only [Value.symbolize?, Prim.symbolize, Option.some.injEq] at hsym    simp only [←hsym, typeOf_term_prim_entity, TermType.ofType, hwt_ety.1]  | instance_of_set s =>    simp only [      Value.symbolize?,      bind, Option.bind,    ] at hsym    split at hsym    contradiction    rename_i sym_elems hsym_elems    simp only [Option.some.injEq] at hsym    simp only [←hsym, Term.typeOf, TermType.ofType]  | instance_of_record rec rty h₁ h₂ h₃ =>    cases hwf_ty with | record_wf hwf_rty_map hwf_rty =>    simp only [      Value.symbolize?,      bind, Option.bind,    ] at hsym    split at hsym    contradiction    rename_i sym_attrs hsym_attrs    simp only [Option.some.injEq] at hsym    simp only [←hsym, Term.typeOf, TermType.ofType]    congr    rw [Map.mapOnValues₂_eq_mapOnValues _ Term.typeOf]    simp only [Map.mapOnValues, Map.toList_mk_id, ofRecordType_as_map, Map.mk.injEq]    have :      List.Forall₂        (λ rty_entry sym_attr =>          rty_entry ∈ rty.toList ∧          .some sym_attr = Value.symbolize?.symbolizeAttr? rec rty_entry.1 rty_entry.2)        (Map.toList rty)        sym_attrs    := by      apply List.mapM_implies_forall₂_option _ hsym_attrs      intros _ _ _ h      constructor      · assumption      · simp [h]    apply Eq.symm    apply List.forall₂_iff_map_eq.mp    apply List.Forall₂.imp _ this    intros rty_entry sym_attr hsym_attr    simp only [Value.symbolize?.symbolizeAttr?] at hsym_attr    have : rty_entry.fst = sym_attr.fst    := by      replace hsym_attr := hsym_attr.2      split at hsym_attr      · simp only [Option.some.injEq] at hsym_attr        simp only [hsym_attr]      · split at hsym_attr        all_goals          simp only [bind, Option.bind] at hsym_attr          split at hsym_attr          contradiction          simp only [Option.some.injEq] at hsym_attr          simp only [hsym_attr]    simp only [this, Prod.mk.injEq, true_and]    have hfind_rty := (Map.in_list_iff_find?_some hwf_rty_map).mp hsym_attr.1    split at hsym_attr    · simp only [Option.some.injEq] at hsym_attr      simp only [hsym_attr]      cases hqty : rty_entry.snd with      | optional =>        simp only [TermType.ofQualifiedType, Qualified.getType, Term.typeOf]      | required =>        rename_i hnot_find_rec _        have := h₃ rty_entry.fst rty_entry.snd hfind_rty        simp only [Qualified.isRequired, hqty, forall_const] at this        simp [Map.contains, hnot_find_rec, Option.isSome] at this    · rename_i attr' hfind_rec      split at hsym_attr      all_goals        rename_i ty' hqty        simp only [bind, Option.bind] at hsym_attr        split at hsym_attr        · have := hsym_attr.2          contradiction        rename_i sym_attr' hsym_attr'        simp only [Option.some.injEq] at hsym_attr        simp only [hsym_attr, hqty, TermType.ofQualifiedType, Term.typeOf]        congr        have hwf_ty' : ty'.WellFormed Γ := by          have := hwf_rty rty_entry.fst rty_entry.snd hfind_rty          simp only [hqty] at this          cases this          assumption        have hwt_v' : InstanceOfType Γ attr' ty' := by          have := h₂ rty_entry.fst _ rty_entry.snd hfind_rec hfind_rty          simp only [hqty, Qualified.getType] at this          exact this        have := value_symbolize?_well_typed          hwf_ty' hwt_v' hsym_attr'        simp [this]  | instance_of_ext ext _ hwt_ext =>    simp only [Value.symbolize?, Option.some.injEq] at hsym    cases ext    all_goals      simp only [←hsym, typeOf_term_prim_ext_datetime, typeOf_term_prim_ext_decimal, typeOf_term_prim_ext_duration, typeOf_term_prim_ext_ipaddr, TermType.ofType]      simp only [InstanceOfExtType] at hwt_ext      split at hwt_ext <;> (try simp) <;> contradiction