+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.
+
+(* XXX move to pair.ma *)
+nlet rec eq_pair (A, B : setoid) (a : A × B) (b : A × B) on a : CProp[0] ≝
+ match a with [ mk_pair a1 a2 ⇒
+ match b with [ mk_pair b1 b2 ⇒ a1 = b1 ∧ a2 = b2 ]].
+
+interpretation "eq_pair" 'eq_low a b = (eq_pair ?? a b).
+
+nlemma PAIR : ∀A,B:setoid. setoid.
+#A B; @(A × B); @(eq_pair …);
+##[ #ab; ncases ab; #a b; @; napply #;
+##| #ab cd; ncases ab; ncases cd; #a1 a2 b1 b2; *; #E1 E2;
+ @; napply (?^-1); //;
+##| #a b c; ncases a; ncases b; ncases c; #c1 c2 b1 b2 a1 a2;
+ *; #E1 E2; *; #E3 E4; @; ##[ napply (.= E1); //] napply (.= E2); //.##]
+nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ AA, BB;
+ A ≟ carr AA, B ≟ carr BB,
+ P1 ≟ refl ? (eq0 (PAIR AA BB)),
+ P2 ≟ sym ? (eq0 (PAIR AA BB)),
+ P3 ≟ trans ? (eq0 (PAIR AA BB)),
+ R ≟ mk_setoid (A × B) (mk_equivalence_relation ? (eq_pair …) P1 P2 P3)
+(*---------------------------------------------------------------------------*)⊢
+ carr R ≡ A × B.
+
+unification hint 0 ≔ S1,S2,a,b;
+ R ≟ PAIR S1 S2,
+ L ≟ (pair S1 S2)
+(* -------------------------------------------- *) ⊢
+ eq_pair S1 S2 a b ≡ eq_rel L (eq0 R) a b.
+
+(* end move to pair *)
+