/2 width=1 by pr_nat_pred_bi/
qed.
(* Inversions with pr_uni ***************************************************)
lemma pr_nat_inv_uni (n) (l) (k):
/2 width=1 by pr_nat_pred_bi/
qed.
(* Inversions with pr_uni ***************************************************)
lemma pr_nat_inv_uni (n) (l) (k):