#g #m * -g -m /2 width=3 by ex2_intro/
[ #g #Hg #f #H elim (isid_inv_next … H) -H //
| #g #m #_ #f #H elim (discr_next_push … H)
#g #m * -g -m /2 width=3 by ex2_intro/
[ #g #Hg #f #H elim (isid_inv_next … H) -H //
| #g #m #_ #f #H elim (discr_next_push … H)