apply Function.updateListITE_mem_eq_len
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v =
    Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ E_hd.args.length = (List.map (V ∘ σ) xs).length