cases f1 -f1 #p1 #f1 cases f2 -f2 #p2 #f2
cases tr_inj_unfold cases tr_inj_unfold #H
cases (pr_eq_inv_nexts_push_bi … H) -H #H1 #H2
cases f1 -f1 #p1 #f1 cases f2 -f2 #p2 #f2
cases tr_inj_unfold cases tr_inj_unfold #H
cases (pr_eq_inv_nexts_push_bi … H) -H #H1 #H2