-definition DeqProd ≝ λA,B:DeqSet.
- mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
+lemma enum_prod_complete:∀A,B:DeqSet.∀l1,l2.
+ (∀a. memb A a l1 = true) → (∀b.memb B b l2 = true) →
+ ∀p. memb ? p (enum_prod A B l1 l2) = true.
+#A #B #l1 #l2 #Hl1 #Hl2 * #a #b @memb_compose //
+qed.
+
+definition FinProd ≝
+λA,B:FinSet.mk_FinSet (DeqProd A B)
+ (enum_prod A B (enum A) (enum B))
+ (enum_prod_unique A B … (enum_unique A) (enum_unique B))
+ (enum_prod_complete A B … (enum_complete A) (enum_complete B)).
+
+unification hint 0 ≔ C1,C2;
+ T1 ≟ FinSetcarr C1,
+ T2 ≟ FinSetcarr C2,
+ X ≟ FinProd C1 C2
+(* ---------------------------------------- *) ⊢
+ T1×T2 ≡ FinSetcarr X.
+
+(* graph of a function *)
+
+definition graph_of ≝ λA,B.λf:A→B.
+ Σp:A×B.f (\fst p) = \snd p.
+
+definition graph_enum ≝ λA,B:FinSet.λf:A→B.
+ filter ? (λp.f (\fst p) == \snd p) (enum (FinProd A B)).