* #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
[ cases n1 -n1
[ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/
* #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
[ cases n1 -n1
[ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/