proposition: Lemma mem_1 : forall m x, In x m -> mem x m = true.
proof: Proof. unfold In, MapsTo; intros m x; rewrite mem_find. destruct 1 as (e0,H0); rewrite H0; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface