split_ifs
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V' E_hd.args (List.map V' xs)) M E_tl E_hd.F
    else Holds D I V' M E_tl (def_ X xs)
case pos
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V' E_hd.args (List.map V' xs)) M E_tl E_hd.F

case neg
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I V' M E_tl (def_ X xs)