apply Exists.elim h1
F : Formula
v u : VarName
binders : Finset VarName
h1 : ∃ F', IsSub F v u F'
h2 : u ∉ binders
⊢ Rec.fastAdmitsAux v u binders F
F : Formula
v u : VarName
binders : Finset VarName
h1 : ∃ F', IsSub F v u F'
h2 : u ∉ binders
⊢ ∀ (a : Formula), IsSub F v u a → Rec.fastAdmitsAux v u binders F