simp only [← s1]
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE V (↑σ x) a ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)