simp only [isFreeIn] at h1_1_1
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
h1_1_1 : ¬isFreeIn h1_1_v (exists_ h1_1_x h1_1_phi)
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
h1_1_1 : ¬(¬h1_1_v = h1_1_x ∧ isFreeIn h1_1_v h1_1_phi)
binders : Finset VarName
h2 : h1_1_t ∉ binders
⊢ h1_1_v = h1_1_x ∨ Rec.fastAdmitsAux h1_1_v h1_1_t (binders ∪ {h1_1_x}) h1_1_phi