tauto
case iff_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), admitsAux v u S a✝¹ → admitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), admitsAux v u S a✝ → admitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : admitsAux v u S a✝¹ ∧ admitsAux v u S a✝
⊢ admitsAux v u (S ∪ T) a✝¹ ∧ admitsAux v u (S ∪ T) a✝
no goals