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