proposition: Lemma in_find_iff : forall m x, In x m <-> find x m <> None.
proof: Proof. intros; rewrite <- not_find_in_iff, mem_in_iff. destruct mem; intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface