Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
case pred_const_
F : Formula
v u : VarName
F' : Formula
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (pred_const_ X✝ xs✝)

case pred_var_
F : Formula
v u : VarName
F' : Formula
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (pred_var_ X✝ xs✝)

case eq_
F : Formula
v u : VarName
F' : Formula
x✝ y✝ v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (eq_ x✝ y✝)

case true_
F : Formula
v u : VarName
F' : Formula
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders true_

case false_
F : Formula
v u : VarName
F' : Formula
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders false_

case not_
F : Formula
v u : VarName
F' phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝.not_

case imp_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (phi✝.imp_ psi✝)

case and_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (phi✝.and_ psi✝)

case or_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (phi✝.or_ psi✝)

case iff_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (phi✝.iff_ psi✝)

case forall_not_free_in
F : Formula
v u : VarName
F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (forall_ x✝ phi✝)
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (forall_ x✝ phi✝)

case forall_free_in
F : Formula
v u : VarName
F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (forall_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (forall_ x✝ phi✝)

case exists_not_free_in
F : Formula
v u : VarName
F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (exists_ x✝ phi✝)
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (exists_ x✝ phi✝)

case exists_free_in
F : Formula
v u : VarName
F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (exists_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (exists_ x✝ phi✝)

case def_
F : Formula
v u : VarName
F' : Formula
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders (def_ X✝ xs✝)
Tactic:
all_goals
  simp only [Rec.fastAdmitsAux]
Proof state after:
case pred_const_
F : Formula
v u : VarName
F' : Formula
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ ∈ xs✝ → t✝ ∉ binders

case pred_var_
F : Formula
v u : VarName
F' : Formula
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ ∈ xs✝ → t✝ ∉ binders

case eq_
F : Formula
v u : VarName
F' : Formula
x✝ y✝ v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ = x✝ ∨ v✝ = y✝ → t✝ ∉ binders

case not_
F : Formula
v u : VarName
F' phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝

case imp_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝ ∧ Rec.fastAdmitsAux v✝ t✝ binders psi✝

case and_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝ ∧ Rec.fastAdmitsAux v✝ t✝ binders psi✝

case or_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝ ∧ Rec.fastAdmitsAux v✝ t✝ binders psi✝

case iff_
F : Formula
v u : VarName
F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders psi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ Rec.fastAdmitsAux v✝ t✝ binders phi✝ ∧ Rec.fastAdmitsAux v✝ t✝ binders psi✝

case forall_not_free_in
F : Formula
v u : VarName
F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (forall_ x✝ phi✝)
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ = x✝ ∨ Rec.fastAdmitsAux v✝ t✝ (binders ∪ {x✝}) phi✝

case forall_free_in
F : Formula
v u : VarName
F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (forall_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ = x✝ ∨ Rec.fastAdmitsAux v✝ t✝ (binders ∪ {x✝}) phi✝

case exists_not_free_in
F : Formula
v u : VarName
F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (exists_ x✝ phi✝)
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ = x✝ ∨ Rec.fastAdmitsAux v✝ t✝ (binders ∪ {x✝}) phi✝

case exists_free_in
F : Formula
v u : VarName
F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (exists_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (binders : Finset VarName), t✝ ∉ binders → Rec.fastAdmitsAux v✝ t✝ binders phi✝
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ = x✝ ∨ Rec.fastAdmitsAux v✝ t✝ (binders ∪ {x✝}) phi✝

case def_
F : Formula
v u : VarName
F' : Formula
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
binders : Finset VarName
h2 : t✝ ∉ binders
⊢ v✝ ∈ xs✝ → t✝ ∉ binders