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

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

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

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

State before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
⊢ ∀ v ∈ ∅, (V ∘ σ) 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 F' : Formula
h1 : IsSub σ F F'
⊢ ∀ (v : VarName), σ v ∉ ∅ → (V ∘ σ) v = V (σ v)
Tactic:
simp
State after:
no goals

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