Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case s1
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
x : VarName
a2 : x ∈ xs'
⊢ V x = (V' ∘ σ') x

case 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
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ Function.updateListITE V hd.args (List.map V xs') v = Function.updateListITE V' hd.args (List.map (V' ∘ σ') xs') v
Tactic:
by_cases c3 : x ∈ binders'
Proof state after:
case pos
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
x : VarName
a2 : x ∈ xs'
c3 : x ∈ binders'
⊢ V x = (V' ∘ σ') x

case neg
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
x : VarName
a2 : x ∈ xs'
c3 : x ∉ binders'
⊢ V x = (V' ∘ σ') x

case 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
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ Function.updateListITE V hd.args (List.map V xs') v = Function.updateListITE V' hd.args (List.map (V' ∘ σ') xs') v