case inl h1 =>
  tauto
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : v = x
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
no goals