proposition: Lemma remove_2 : forall m (Hm:Sort m) x y e, ~ eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
proof: Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo. functional induction (remove x m);subst;auto; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac end. inversion_clear 3; auto. compute in H1; destruct H1. subst; now contradict H. inversion_clear 1; inversion_clear 2; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses