intro v a1
case h.h2
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
⊢ ∀ v ∈ x :: vs, Function.updateITE V x a v = Function.updateITE V' x a v
case h.h2
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
⊢ Function.updateITE V x a v = Function.updateITE V' x a v