(*** at_uni *)
lemma pr_pat_uni (n) (i):
- @â\9dªi,ð\9d\90®â\9d¨nâ\9d©â\9d« ≘ i+n.
+ @â\9d¨i,ð\9d\90®â\9d¨nâ\9d©â\9d© ≘ i+n.
#n @(nat_ind_succ … n) -n
/2 width=5 by pr_pat_next/
qed.
(*** at_inv_uni *)
lemma pr_pat_inv_uni (n) (i) (j):
- @â\9dªi,ð\9d\90®â\9d¨nâ\9d©â\9d« ≘ j → j = i+n.
+ @â\9d¨i,ð\9d\90®â\9d¨nâ\9d©â\9d© ≘ j → j = i+n.
/2 width=4 by pr_pat_mono/ qed-.