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

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

State before:
F : Formula
v : VarName
⊢ admitsAux v v ∅ F
Tactic:
apply admitsAux_self
State after:
no goals