#f cases (pn_split f) * #g #Hg #H
[ lapply (sdj_inv_pp … H … Hg Hg) -H /3 width=3 by isid_push/
| elim (sdj_inv_nn … H … Hg Hg)
#f cases (pn_split f) * #g #Hg #H
[ lapply (sdj_inv_pp … H … Hg Hg) -H /3 width=3 by isid_push/
| elim (sdj_inv_nn … H … Hg Hg)