tauto
case h.h2
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
phi'✝ : Formula
a✝¹ : isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
h1_1_2 : ¬h1_1_x = h1_1_t
a✝ : IsSub h1_1_phi h1_1_v h1_1_t phi'✝
h1_1_ih : ∀ (binders : Finset VarName), h1_1_t ∉ binders → Rec.fastAdmitsAux h1_1_v h1_1_t binders h1_1_phi
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_t ∉ binders ∧ ¬h1_1_t = h1_1_x
no goals