(* Advanced constructions with pr_pat ***************************************)
(*** at_dec *)
-lemma pr_pat_dec (f) (i1) (i2): ð\9d\90\93â\9dªfâ\9d« â\86\92 Decidable (@â\9dªi1,fâ\9d« ≘ i2).
+lemma pr_pat_dec (f) (i1) (i2): ð\9d\90\93â\9d¨fâ\9d© â\86\92 Decidable (@â\9d¨i1,fâ\9d© ≘ i2).
#f #i1 #i2 #Hf lapply (Hf i1) -Hf *
#j2 #Hf elim (eq_pnat_dec i2 j2)
[ #H destruct /2 width=1 by or_introl/
qed-.
(*** is_at_dec *)
-lemma is_pr_pat_dec (f) (i2): ð\9d\90\93â\9dªfâ\9d« â\86\92 Decidable (â\88\83i1. @â\9dªi1,fâ\9d« ≘ i2).
+lemma is_pr_pat_dec (f) (i2): ð\9d\90\93â\9d¨fâ\9d© â\86\92 Decidable (â\88\83i1. @â\9d¨i1,fâ\9d© ≘ i2).
#f #i2 #Hf
-lapply (dec_plt (λi1.@â\9dªi1,fâ\9d« ≘ i2) … (↑i2)) [| * ]
+lapply (dec_plt (λi1.@â\9d¨i1,fâ\9d© ≘ i2) … (↑i2)) [| * ]
[ /2 width=1 by pr_pat_dec/
| * /3 width=2 by ex_intro, or_introl/
| #H @or_intror * #i1 #Hi12
(* Main destructions with pr_pat ********************************************)
(*** at_ext *)
-corec theorem pr_eq_ext_pat (f1) (f2): ð\9d\90\93â\9dªf1â\9d« â\86\92 ð\9d\90\93â\9dªf2â\9d« →
- (â\88\80i,i1,i2. @â\9dªi,f1â\9d« â\89\98 i1 â\86\92 @â\9dªi,f2â\9d« ≘ i2 → i1 = i2) →
+corec theorem pr_eq_ext_pat (f1) (f2): ð\9d\90\93â\9d¨f1â\9d© â\86\92 ð\9d\90\93â\9d¨f2â\9d© →
+ (â\88\80i,i1,i2. @â\9d¨i,f1â\9d© â\89\98 i1 â\86\92 @â\9d¨i,f2â\9d© ≘ i2 → i1 = i2) →
f1 ≡ f2.
cases (pr_map_split_tl f1) #H1
cases (pr_map_split_tl f2) #H2
(* Advanced constructions with pr_nat ***************************************)
-lemma is_pr_nat_dec (f) (l2): ð\9d\90\93â\9dªfâ\9d« â\86\92 Decidable (â\88\83l1. @â\86\91â\9dªl1,fâ\9d« ≘ l2).
+lemma is_pr_nat_dec (f) (l2): ð\9d\90\93â\9d¨fâ\9d© â\86\92 Decidable (â\88\83l1. @â\86\91â\9d¨l1,fâ\9d© ≘ l2).
#f #l2 #Hf elim (is_pr_pat_dec … (↑l2) Hf)
[ * /3 width=2 by ex_intro, or_introl/
| #H @or_intror * /3 width=2 by ex_intro/