Value symbolize? wf

theorem value_symbolize?_wf  {Γ : TypeEnv} {env : Env}  {v : Value} {ty : CedarType} {t : Term}  (hinst : InstanceOfWellFormedEnvironment env.request env.entities Γ)  (hwf_ty : ty.WellFormed Γ)  (hwf_v : v.WellFormed env.entities)  (hwt_v : InstanceOfType Γ v ty)  (hsym : v.symbolize? ty = .some t) :  t.WellFormed (SymEnv.ofEnv Γ).entities:= by  have ⟨hwf_Γ, _, _⟩ := hinst  cases v with  | prim p =>    cases p with    | bool | int | string =>      simp only [Value.symbolize?, Prim.symbolize, Option.some.injEq] at hsym      simp only [←hsym]      repeat constructor    | entityUID uid =>      simp only [Value.symbolize?, Prim.symbolize, Option.some.injEq] at hsym      simp only [←hsym]      constructor      constructor      cases hwf_v with | prim_wf hwf_prim =>      simp only [Prim.WellFormed] at hwf_prim      exact env_valid_uid_implies_sym_env_valid_uid hinst hwf_prim  | set s =>    cases s with | mk elems =>    cases hwf_v with | set_wf hwf_elems =>    unfold Value.symbolize? at hsym    split at hsym    any_goals contradiction    rename_i s' elem_ty heq    simp only [Value.set.injEq] at heq    simp only [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]    cases hwf_ty with | set_wf hwf_elem_ty =>    -- Obligations of `Term.WellFormed` for `.set`    constructor    · intros t hmem_t      simp only [List.mapM₁_eq_mapM (λ x => x.symbolize? elem_ty) s'.toList] at hsym_elems      have ⟨elem, hmem_elem, hsym_elem⟩ := List.mapM_some_implies_all_from_some        hsym_elems t ((Set.mem_make _ _).mp hmem_t)      simp only [←heq] at hmem_elem      have hwf_elem := hwf_elems elem hmem_elem      cases hwt_v with | instance_of_set _ _ hwt_elem =>      specialize hwt_elem elem hmem_elem      exact value_symbolize?_wf hinst hwf_elem_ty hwf_elem hwt_elem hsym_elem    · intros t hmem_t      simp only [List.mapM₁_eq_mapM (λ x => x.symbolize? elem_ty) s'.toList] at hsym_elems      have ⟨elem, hmem_elem, hsym_elem⟩ := List.mapM_some_implies_all_from_some        hsym_elems t ((Set.mem_make _ _).mp hmem_t)      simp only [←heq] at hmem_elem      have hwf_elem := hwf_elems elem hmem_elem      cases hwt_v with | instance_of_set _ _ hwt_elem =>      specialize hwt_elem elem hmem_elem      exact value_symbolize?_well_typed hwf_elem_ty hwt_elem hsym_elem    · exact ofType_wf hwf_Γ hwf_elem_ty    · exact Set.make_wf _  | record rec =>    cases rec with | mk attrs =>    cases hwf_v with | record_wf hwf_attrs hwf_attrs_map =>    unfold Value.symbolize? at hsym    split at hsym    any_goals contradiction    rename_i rec' rty heq_rec'    simp only [Value.record.injEq] at heq_rec'    simp only [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]    cases hwf_ty with | record_wf hwf_rty_map hwf_rty =>    cases rty with | mk rty_map =>    -- Obligations of `Term.WellFormed` for `.record`    constructor    · intros attr t hmem_attr_t      have ⟨attr_term, hmem_attr_term, hsym_attr_term⟩ :=        List.mapM_some_implies_all_from_some hsym_attrs (attr, t) hmem_attr_t      simp only [Value.symbolize?.symbolizeAttr?] at hsym_attr_term      simp only [bind, Option.bind] at hsym_attr_term      simp only [Map.toList_mk_id] at hmem_attr_t      split at hsym_attr_term      · simp only [Option.some.injEq, Prod.mk.injEq] at hsym_attr_term        simp only [←hsym_attr_term.2]        constructor        have hfind_attr_term := (Map.in_list_iff_find?_some hwf_rty_map).mp hmem_attr_term        have := hwf_rty _ _ hfind_attr_term        cases hqty : attr_term.snd        all_goals          simp only [hqty] at this          cases this          simp only [Qualified.getType]          apply ofType_wf hwf_Γ          assumption      · rename_i val hfind_rec'        simp only [←heq_rec'] at hfind_rec'        split at hsym_attr_term        all_goals          rename_i ty' hty'          split at hsym_attr_term          contradiction          rename_i sym_val hsym_val          simp only [Option.some.injEq, Prod.mk.injEq] at hsym_attr_term          simp only [←hsym_attr_term.2]          try constructor          have hwf_ty' : CedarType.WellFormed Γ ty' := by            have hfind_attr := (Map.in_list_iff_find?_some hwf_rty_map).mp hmem_attr_term            have := hwf_rty _ _ hfind_attr            simp only [hty'] at this            cases this            assumption          have hwf_val : val.WellFormed env.entities := hwf_attrs _ _ hfind_rec'          have hwt_val : InstanceOfType Γ val ty' := by            cases hwt_v with | instance_of_record _ _ _ hwt_attr =>            have hfind_rty_attr := (Map.in_list_iff_find?_some hwf_rty_map).mp hmem_attr_term            simp only [hty'] at hfind_rty_attr            exact hwt_attr _ _ _ hfind_rec' hfind_rty_attr          exact value_symbolize?_wf hinst hwf_ty' hwf_val hwt_val hsym_val    · apply Map.mk_wf      have hsorted_rty_map :        List.SortedBy Prod.fst rty_map      := Map.wf_iff_sorted.mp hwf_rty_map      -- TODO: merge this with `hsorted_sym_attrs`?      apply List.mapM_preserves_SortedBy hsorted_rty_map hsym_attrs      unfold Value.symbolize?.symbolizeAttr?      intros a b      split      · simp only [Option.some.injEq]        intros h        simp [←h]      · split        all_goals          simp only [bind, Option.bind]          split          · simp          · simp only [Option.some.injEq]            intros h            simp [←h]  | ext =>    simp only [Value.symbolize?, Option.some.injEq] at hsym    simp only [←hsym]    repeat constructor