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

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

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