Valid Refs invariant under lift Bool Types

theorem ValidRefs_invariant_under_liftBoolTypes  {tx : TypedExpr} {f : EntityUID → Prop}  (hrefs : tx.liftBoolTypes.toExpr.ValidRefs f) :  tx.toExpr.ValidRefs f:= by  cases tx with  | lit p ty =>    cases p with    | bool | int | string =>      simp only [TypedExpr.toExpr]      constructor      constructor    | entityUID uid =>      simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢      exact hrefs  | var =>    simp only [TypedExpr.toExpr]    constructor  | ite tx₁ tx₂ tx₃ ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | ite_valid h₁ h₂ h₃ =>    constructor    exact ValidRefs_invariant_under_liftBoolTypes h₁    exact ValidRefs_invariant_under_liftBoolTypes h₂    exact ValidRefs_invariant_under_liftBoolTypes h₃  | and tx₁ tx₂ ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | and_valid h₁ h₂ =>    constructor    exact ValidRefs_invariant_under_liftBoolTypes h₁    exact ValidRefs_invariant_under_liftBoolTypes h₂  | or tx₁ tx₂ ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | or_valid h₁ h₂ =>    constructor    exact ValidRefs_invariant_under_liftBoolTypes h₁    exact ValidRefs_invariant_under_liftBoolTypes h₂  | unaryApp tx f ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | unaryApp_valid h =>    constructor    exact ValidRefs_invariant_under_liftBoolTypes h  | hasAttr tx attr ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | hasAttr_valid h =>    constructor    exact ValidRefs_invariant_under_liftBoolTypes h  | getAttr tx attr ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | getAttr_valid h =>    constructor    exact ValidRefs_invariant_under_liftBoolTypes h  | binaryApp tx₁ tx₂ f ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | binaryApp_valid h₁ h₂ =>    constructor    exact ValidRefs_invariant_under_liftBoolTypes h₁    exact ValidRefs_invariant_under_liftBoolTypes h₂  | set txs ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | set_valid h =>    constructor    intros x hmem_x    simp only [List.map₁_eq_map] at hmem_x    simp only [      List.map₁_eq_map,      List.map_map, List.mem_map,      Function.comp_apply, forall_exists_index, and_imp,      forall_apply_eq_imp_iff₂,    ] at h    have ⟨tx, hmem_tx, htx⟩ := List.mem_map.mp hmem_x    have := h tx hmem_tx    simp only [←htx]    exact ValidRefs_invariant_under_liftBoolTypes this  | call txs ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | call_valid h =>    constructor    intros x hmem_x    simp only [List.map₁_eq_map] at hmem_x    simp only [      List.map₁_eq_map,      List.map_map, List.mem_map,      Function.comp_apply, forall_exists_index, and_imp,      forall_apply_eq_imp_iff₂,    ] at h    have ⟨tx, hmem_tx, htx⟩ := List.mem_map.mp hmem_x    have := h tx hmem_tx    simp only [←htx]    exact ValidRefs_invariant_under_liftBoolTypes this  | record attrs ty =>    simp only [TypedExpr.toExpr, TypedExpr.liftBoolTypes] at hrefs ⊢    cases hrefs with | record_valid h =>    constructor    intros attr hmem_attr    simp only [List.map₂_eq_map_snd] at hmem_attr h    simp only [      List.map_map, List.mem_map,      Function.comp_apply, Prod.exists,      forall_exists_index, and_imp,      Prod.forall, Prod.mk.injEq,    ] at h    have ⟨⟨attr', tx⟩, hmem_attr'_tx, hattr'_tx⟩ := List.mem_map.mp hmem_attr    simp only at hattr'_tx    simp only [←hattr'_tx]    have := h attr' tx.liftBoolTypes.toExpr attr' tx hmem_attr'_tx rfl rfl    exact ValidRefs_invariant_under_liftBoolTypes this