proposition: Lemma cardinal_0 : forall s, exists l : list elt, NoDupA E.eq l /\ (forall x : elt, In x s <-> InA E.eq x l) /\ cardinal s = length l.
proof: Proof. intros; exists (elements s); intuition auto with set; apply cardinal_1. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide