(* Constructions with pr_uni ************************************************)
lemma pr_nat_uni (n) (l):
- @â\86\91â\9dªl,ð\9d\90®â\9d¨nâ\9d©â\9d« ≘ l+n.
+ @â\86\91â\9d¨l,ð\9d\90®â\9d¨nâ\9d©â\9d© ≘ l+n.
/2 width=1 by pr_nat_pred_bi/
qed.
(* Inversions with pr_uni ***************************************************)
lemma pr_nat_inv_uni (n) (l) (k):
- @â\86\91â\9dªl,ð\9d\90®â\9d¨nâ\9d©â\9d« ≘ k → k = l+n.
+ @â\86\91â\9d¨l,ð\9d\90®â\9d¨nâ\9d©â\9d© ≘ k → k = l+n.
/2 width=4 by pr_nat_mono/ qed-.