proposition: Lemma not_mem_in_iff : forall m x, ~In x m <-> mem x m = false.
proof: Proof. intros; rewrite mem_in_iff; destruct (mem x m); intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface