Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
case pred_const_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : PredName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → u ∉ S ∪ T

case pred_var_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : PredName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → u ∉ S ∪ T

case eq_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : VarName
S : Finset VarName
h1 : v = a✝¹ ∨ v = a✝ → u ∉ S
⊢ v = a✝¹ ∨ v = a✝ → u ∉ S ∪ T

case not_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝ : Formula
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝

case imp_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

case and_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

case or_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

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

case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → u ∉ S ∪ T
Tactic:
any_goals
  simp only [Finset.mem_union]
Proof state after:
case pred_const_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : PredName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → ¬(u ∈ S ∨ u ∈ T)

case pred_var_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : PredName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → ¬(u ∈ S ∨ u ∈ T)

case eq_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : VarName
S : Finset VarName
h1 : v = a✝¹ ∨ v = a✝ → u ∉ S
⊢ v = a✝¹ ∨ v = a✝ → ¬(u ∈ S ∨ u ∈ T)

case not_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝ : Formula
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝

case imp_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

case and_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

case or_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

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

case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → ¬(u ∈ S ∨ u ∈ T)