#n @(nat_ind_succ … n) -n
[ #g <pr_uni_zero <pr_id_unfold #H elim (pr_eq_inv_push_next … H) -H //
| #n #_ #g <pr_uni_succ /3 width=5 by pr_eq_inv_next_bi, conj/
#n @(nat_ind_succ … n) -n
[ #g <pr_uni_zero <pr_id_unfold #H elim (pr_eq_inv_push_next … H) -H //
| #n #_ #g <pr_uni_succ /3 width=5 by pr_eq_inv_next_bi, conj/