proposition: Lemma In_dec : forall x s, {In x s} + {~ In x s}.
proof: Proof. intros; generalize (mem_iff s x); case (mem x s); intuition auto with bool. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide