apply substitution_theorem_aux D I (V ∘ σ) V E σ σ ∅ F h1
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)
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