proposition: Lemma In_dec m x : { In x m } + { ~ In x m }.
proof: Proof. generalize (mem_in_iff m x). destruct (mem x m); [left|right]; intuition discriminate. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)