apply Function.updateListITE_map_mem_ext
case h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ 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
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ ∀ y ∈ xs, (V ∘ σ) y = (V ∘ σ) y

case h1.h2
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ E_hd.args.length = xs.length

case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ v ∈ E_hd.args