exact s2
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
a1 : v ∈ hd.q.freeVarSet
s2 : v ∈ hd.args
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length