(*** at_uni *)
lemma pr_pat_uni (n) (i):
- @❪i,𝐮❨n❩❫ ≘ i+n.
+ @⧣❨i,𝐮❨n❩❩ ≘ 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):
- @❪i,𝐮❨n❩❫ ≘ j → j = i+n.
+ @⧣❨i,𝐮❨n❩❩ ≘ j → j = i+n.
/2 width=4 by pr_pat_mono/ qed-.