apply IsSub.imp_
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.imp_ psi) v u ((Rec.fastReplaceFree v u phi).imp_ (Rec.fastReplaceFree v u psi))
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)