subst c1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : x = v
c2 : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
V : Valuation D
d d' : D
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
phi_ih :
  NotFree Γ x phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V x d) M E phi
c2 : NotFree Γ x phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d) x d') M E phi