Type Of preserves valid refs

theorem typeOf_preserves_valid_refs  {Γ : TypeEnv} (entities : Entities)  {expr : Expr} {tx : TypedExpr} {c₁ c₂ : Capabilities}  (hty : typeOf expr c₁ Γ = Except.ok (tx, c₂))  (hrefs : entities.ValidRefsFor expr) :  entities.ValidRefsFor tx.toExpr:= by  cases expr with  | lit p => exact typeOf_preserves_valid_refs_lit entities hty hrefs  | var v => exact typeOf_preserves_valid_refs_var entities hty hrefs  | and e₁ e₂ =>    apply typeOf_preserves_valid_refs_and entities hty hrefs    · intros tx c c'; apply typeOf_preserves_valid_refs    · intros tx c c'; apply typeOf_preserves_valid_refs  | or e₁ e₂ =>    apply typeOf_preserves_valid_refs_or entities hty hrefs    · intros tx c c'; apply typeOf_preserves_valid_refs    · intros tx c c'; apply typeOf_preserves_valid_refs  | ite e₁ e₂ e₃ =>    apply typeOf_preserves_valid_refs_ite entities hty hrefs    · intros tx c c'; apply typeOf_preserves_valid_refs    · intros tx c c'; apply typeOf_preserves_valid_refs    · intros tx c c'; apply typeOf_preserves_valid_refs  | unaryApp _ e =>    apply typeOf_preserves_valid_refs_unaryApp entities hty hrefs    intros tx c c'; apply typeOf_preserves_valid_refs  | binaryApp _ e₁ e₂ =>    apply typeOf_preserves_valid_refs_binaryApp entities hty hrefs    · intros tx c c'; apply typeOf_preserves_valid_refs    · intros tx c c'; apply typeOf_preserves_valid_refs  | getAttr e _ =>    apply typeOf_preserves_valid_refs_getAttr entities hty hrefs    intros tx c c'; apply typeOf_preserves_valid_refs  | hasAttr e _ =>    apply typeOf_preserves_valid_refs_hasAttr entities hty hrefs    intros tx c c'; apply typeOf_preserves_valid_refs  | set s =>    apply typeOf_preserves_valid_refs_set entities hty hrefs    intros x hmem_x tx c c'    apply typeOf_preserves_valid_refs  | call _ args =>    apply typeOf_preserves_valid_refs_call entities hty hrefs    intros arg hmem_arg tx c c'    apply typeOf_preserves_valid_refs  | record rec =>    apply typeOf_preserves_valid_refs_record entities hty hrefs    intros attr hmem_attr tx c c'    apply typeOf_preserves_valid_refs