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

State before:
F : Formula
v u : VarName
binders : Finset VarName
h1 : fastAdmitsAux v u binders F
h2 : u ∈ binders
⊢ ¬isFreeIn v F
Tactic:
contrapose! h2
State after:
F : Formula
v u : VarName
binders : Finset VarName
h1 : fastAdmitsAux v u binders F
h2 : isFreeIn v F
⊢ u ∉ binders

State before:
F : Formula
v u : VarName
binders : Finset VarName
h1 : fastAdmitsAux v u binders F
h2 : isFreeIn v F
⊢ u ∉ binders
Tactic:
exact fastAdmitsAux_isFreeIn F v u binders h1 h2
State after:
no goals