elim (gr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
elim (gr_coafter_inv_next_sn … Hf … H1) -Hf #g #Hg #H0
lapply (IH … Hg1 … Hg) -i2 -Hg
elim (gr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
elim (gr_coafter_inv_next_sn … Hf … H1) -Hf #g #Hg #H0
lapply (IH … Hg1 … Hg) -i2 -Hg