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