+axiom 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.
+
+lemma enumAB_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.
+
+definition FinSum ≝ λA,B:FinSet.
+ mk_FinSet (DeqSum A B)
+ (enum_sum A B (enum A) (enum B))
+ (enumAB_unique … (enum_unique A) (enum_unique B)).
+
+unification hint 0 ≔ C1,C2;
+ T1 ≟ FinSetcarr C1,
+ T2 ≟ FinSetcarr C2,
+ X ≟ FinSum C1 C2
+(* ---------------------------------------- *) ⊢
+ T1+T2 ≡ FinSetcarr X.
+
+
+(*