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

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

State before:
F : Formula
v u : VarName
h1 : ¬isFreeIn v F
⊢ admitsAux v u ∅ F
Tactic:
exact not_isFreeIn_imp_admitsAux F v u ∅ h1
State after:
no goals