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