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

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

State before:
F : Formula
v : VarName
⊢ fastAdmitsAux v v ∅ F
Tactic:
apply fastAdmitsAux_self
State after:
case h1
F : Formula
v : VarName
⊢ v ∉ ∅

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