intro a
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)