proposition: Lemma mem_find : forall m x, mem x m = match find x m with None => false | _ => true end.
proof: Proof. induction m; destruct x; simpl; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface