proposition: Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
proof: Proof. intros m; apply Raw.find_1; auto. apply m.(sorted). Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses