exact phi_ih binders h1
case a
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
no goals