Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem (FOL/NV/Sub/Var/All/Rec/Admits.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ Holds D I (V ∘ σ) E F ↔ Holds D I V E (fastReplaceFree σ F)
Tactic:
apply substitution_theorem_aux D I (V ∘ σ) V E σ σ ∅ F h1
State after:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ (v : VarName), v ∈ ∅ ∨ σ v ∉ ∅ → (V ∘ σ) v = V (σ v)

case h2'
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ v ∈ ∅, v = σ v

case h3
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ v ∉ ∅, σ v = σ v

State before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ (v : VarName), v ∈ ∅ ∨ σ v ∉ ∅ → (V ∘ σ) v = V (σ v)
Tactic:
simp
State after:
no goals

State before:
case h2'
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ v ∈ ∅, v = σ v
Tactic:
simp
State after:
no goals

State before:
case h3
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ v ∉ ∅, σ v = σ v
Tactic:
simp
State after:
no goals