proposition: Lemma In_dec : forall m x, { In x m } + { ~ In x m }.
proof: Proof. intros. generalize (mem_in_iff m x). destruct (mem x m); [left|right]; intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface