+interpretation "pempty" 'empty_r = (pz ?).
+
+(* setoids for pitem *)
+nlet rec eq_pitem (S : Alpha) (p1, p2 : pitem S) on p1 : CProp[0] ≝
+ match p1 with
+ [ pz ⇒ match p2 with [ pz ⇒ True | _ ⇒ False]
+ | pe ⇒ match p2 with [ pe ⇒ True | _ ⇒ False]
+ | ps x ⇒ match p2 with [ ps y ⇒ x = y | _ ⇒ False]
+ | pp x ⇒ match p2 with [ pp y ⇒ x = y | _ ⇒ False]
+ | pc a1 a2 ⇒ match p2 with [ pc b1 b2 ⇒ eq_pitem ? a1 b1 ∧ eq_pitem ? a2 b2| _ ⇒ False]
+ | po a1 a2 ⇒ match p2 with [ po b1 b2 ⇒ eq_pitem ? a1 b1 ∧ eq_pitem ? a2 b2| _ ⇒ False]
+ | pk a ⇒ match p2 with [ pk b ⇒ eq_pitem ? a b | _ ⇒ False]].
+
+interpretation "eq_pitem" 'eq_low a b = (eq_pitem ? a b).
+
+nlemma PITEM : ∀S:Alpha.setoid.
+#S; @(pitem S); @(eq_pitem …);
+##[ #p; nelim p; //; nnormalize; #; @; //;
+##| #p; nelim p; ##[##1,2: #y; ncases y; //; ##|##3,4: #x y; ncases y; //; #; napply (?^-1); nassumption;
+ ##|##5,6: #r1 r2 H1 H2 p2; ncases p2; //; #s1 s2; nnormalize; *; #; @; /2/;
+ ##| #r H y; ncases y; //; nnormalize; /2/;##]
+##| #x; nelim x;
+ ##[ ##1,2: #y z; ncases y; ncases z; //; nnormalize; #; ncases (?:False); //;
+ ##| ##3,4: #a; #y z; ncases y; ncases z; /2/; nnormalize; #; ncases (?:False); //;
+ ##| ##5,6: #r1 r2 H1 H2 y z; ncases y; ncases z; //; nnormalize;
+ ##[##1,2,5,6,7,8,4,10: #; ncases (?:False); //;##]
+ #r1 r2 r3 r4; nnormalize; *; #H1 H2; *; #H3 H4; /3/;
+ ##| #r H y z; ncases y; ncases z; //; nnormalize; ##[##1,2,3,4: #; ncases (?:False); //]
+ #r2 r3; /3/; ##]##]
+nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ SS:Alpha;
+ S ≟ acarr SS,
+ A ≟ carr S,
+ P1 ≟ refl ? (eq0 (PITEM SS)),
+ P2 ≟ sym ? (eq0 (PITEM SS)),
+ P3 ≟ trans ? (eq0 (PITEM SS)),
+ R ≟ mk_setoid (pitem S) (mk_equivalence_relation (pitem A) (eq_pitem SS) P1 P2 P3)
+(*---------------------------*)⊢
+ carr R ≡ pitem A.
+
+unification hint 0 ≔ S:Alpha,a,b:pitem S;
+ R ≟ PITEM S,
+ L ≟ (pitem S)
+(* -------------------------------------------- *) ⊢
+ eq_pitem S a b ≡ eq_rel L (eq0 R) a b.
+
+(* end setoids for pitem *)
+
+ndefinition pre ≝ λS.pitem S × bool.
+
+notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
+interpretation "fst" 'fst x = (fst ? ? x).
+notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
+interpretation "snd" 'snd x = (snd ? ? x).