+lemma enum_sum_def : ∀A,B:FinSet.∀l1,l2. enum_sum A B l1 l2 =
+ (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
+// qed.
+
+lemma enum_sum_unique: ∀A,B:DeqSet.∀l1,l2.
+ uniqueb A l1 = true → uniqueb B l2 = true →
+ uniqueb ? (enum_sum A B l1 l2) = true.
+#A #B #l1 #l2 elim l1
+ [#_ #ul2 @unique_map_inj // #b1 #b2 #Hinr destruct //
+ |#a #tl #Hind #uA #uB @true_to_andb_true
+ [@sym_eq @noteq_to_eqnot % #H
+ cases (memb_append … (sym_eq … H))
+ [#H1 @(absurd (memb ? a tl = true))
+ [@(memb_map_inj …H1) #a1 #a2 #Hinl destruct //
+ |<(andb_true_l … uA) @eqnot_to_noteq //
+ ]
+ |elim l2
+ [normalize #H destruct
+ |#b #tlB #Hind #membH cases (orb_true_l … membH)
+ [#H lapply (\P H) #H1 destruct |@Hind]
+ ]
+ ]
+ |@Hind // @(andb_true_r … uA)
+ ]
+ ]
+qed.
+
+lemma enum_sum_complete: ∀A,B:DeqSet.∀l1,l2.
+ (∀x:A. memb A x l1 = true) →
+ (∀x:B. memb B x l2 = true) →
+ ∀x:DeqSum A B. memb ? x (enum_sum A B l1 l2) = true.
+#A #B #l1 #l2 #Hl1 #Hl2 *
+ [#a @memb_append_l1 @memb_map @Hl1
+ |#b @memb_append_l2 @memb_map @Hl2
+ ]
+qed.
+
+definition FinSum ≝ λA,B:FinSet.
+ mk_FinSet (DeqSum A B)
+ (enum_sum A B (enum A) (enum B))
+ (enum_sum_unique … (enum_unique A) (enum_unique B))
+ (enum_sum_complete … (enum_complete A) (enum_complete B)).
+
+include alias "basics/types.ma".
+