#n @(nat_ind_succ … n) -n /3 width=3 by pr_isi_push/
qed.
(* Inversions with pr_pushs *************************************************)
(*** isid_inv_pushs *)
#n @(nat_ind_succ … n) -n /3 width=3 by pr_isi_push/
qed.
(* Inversions with pr_pushs *************************************************)
(*** isid_inv_pushs *)