-(*
-unification hint 0 ≔ ;
- X ≟ mk_DeqSet bool beqb beqb_true
-(* ---------------------------------------- *) ⊢
- bool ≡ carr X.
-
-unification hint 0 ≔ b1,b2:bool;
- X ≟ mk_DeqSet bool beqb beqb_true
-(* ---------------------------------------- *) ⊢
- beqb b1 b2 ≡ eqb X b1 b2.
-
-example exhint: ∀b:bool. (b == false) = true → b = false.
-#b #H @(\P H).
-qed.
-
-(* pairs *)
-definition eq_pairs ≝
- λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
+definition enum_prod ≝ λA,B:DeqSet.λl1.λl2.
+ compose ??? (mk_Prod A B) l1 l2.
+
+axiom enum_prod_unique: ∀A,B,l1,l2.
+ uniqueb A l1 = true → uniqueb B l2 = true →
+ uniqueb ? (enum_prod A B l1 l2) = true.