Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmits (FOL/NV/Sub/Var/One/Rec/Admits.lean)

State before:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ fastAdmits v u F
Tactic:
simp only [fastAdmits]
State after:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ fastAdmitsAux v u ∅ F

State before:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ fastAdmitsAux v u ∅ F
Tactic:
apply not_isBoundIn_imp_fastAdmitsAux F v u ∅ h1
State after:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ u ∉ ∅

State before:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ u ∉ ∅
Tactic:
simp
State after:
no goals