apply holds_coincide_var D I (Function.updateListITE V E_hd.args (List.map V xs)) (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M E_tl E_hd.F E_hd.args E_hd.nf
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : 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 (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M
      E_tl E_hd.F
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ v_1 ∈ E_hd.args,
    Function.updateListITE V E_hd.args (List.map V xs) v_1 =
      Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs) v_1