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

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

State before:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ admitsAux v u ∅ F
Tactic:
apply not_isBoundIn_imp_admitsAux 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