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