+
+lemma memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f →
+ memb ? (f a) (map ?? f l) = true → memb ? a l = true.
+#A #B #f #l #a #injf elim l
+ [normalize //
+ |#a1 #tl #Hind #Ha cases (orb_true_l … Ha)
+ [#eqf @orb_true_r1 @(\b ?) >(injf … (\P eqf)) //
+ |#membtl @orb_true_r2 /2/
+ ]
+ ]
+qed.
+
+lemma unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f →
+ uniqueb A l = true → uniqueb B (map ?? f l) = true .
+#A #B #f #l #injf elim l
+ [normalize //
+ |#a #tl #Hind #Htl @true_to_andb_true
+ [@sym_eq @noteq_to_eqnot @sym_not_eq
+ @(not_to_not ?? (memb_map_inj … injf …) )
+ <(andb_true_l ?? Htl) /2/
+ |@Hind @(andb_true_r ?? Htl)
+ ]
+ ]
+qed.
+
+record FinSet : Type[1] ≝
+{ FinSetcarr:> DeqSet;
+ enum: list FinSetcarr;
+ enum_unique: uniqueb FinSetcarr enum = true;
+ enum_complete : ∀x:FinSetcarr. memb ? x enum = true}.
+
+(* The library provides many operations for building new FinSet by composing
+existing ones: for example, if A and B have type FinSet, then also option A,
+A × B and A + B are finite sets. In all these cases, unification hints are used
+to suggest the intended finite set structure associated with them, that makes
+their use quite transparent to the user.*)
+
+definition enum_prod ≝ λA,B:DeqSet.λl1:list A.λl2:list B.
+ compose ??? (pair A B) l1 l2.
+
+lemma enum_prod_unique: ∀A,B,l1,l2.
+ uniqueb A l1 = true → uniqueb B l2 = true →
+ uniqueb ? (enum_prod A B l1 l2) = true.
+#A #B #l1 elim l1 //
+ #a #tl #Hind #l2 #H1 #H2 @uniqueb_append
+ [@unique_map_inj // #b1 #b2 #H3 destruct (H3) //
+ |@Hind // @(andb_true_r … H1)
+ |#p #H3 cases (memb_map_to_exists … H3) #b *
+ #Hmemb #eqp <eqp @(not_to_not ? (memb ? a tl = true))
+ [2: @sym_not_eq @eqnot_to_noteq @sym_eq @(andb_true_l … H1)
+ |elim tl
+ [normalize //
+ |#a1 #tl1 #Hind2 #H4 cases (memb_append … H4) -H4 #H4
+ [cases (memb_map_to_exists … H4) #b1 * #memb1 #H destruct (H)
+ normalize >(\b (refl ? a)) //
+ |@orb_true_r2 @Hind2 @H4
+ ]
+ ]
+ ]
+ ]
+qed.
+
+
+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.
+
+(* A particularly intersting case is that of the arrow type A → B. We may define
+the graph of f:A → B, as the set (sigma type) of all pairs 〈a,b〉 such that
+f a = b. *)
+
+definition graph_of ≝ λA,B.λf:A→B. Σp:A×B.f (fst … p) = snd … p.
+
+(* In case the equality is decidable, we may effectively enumerate all elements
+of the graph by simply filtering from pairs in A × B those satisfying the
+test λp.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)).
+
+(* The proofs that this enumeration does not contain repetitions and
+is complete are straightforward. *)