tauto
v u : VarName
T : Finset VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) phi → fastAdmitsAux v u S phi
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ T) phi
⊢ fastAdmitsAux v u S phi
no goals