proposition: Lemma remove_3 : forall m (Hm:Sort m) x y e, MapsTo y e (remove x m) -> MapsTo y e m.
proof: Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo. functional induction (remove x m);subst;auto. inversion_clear 1; inversion_clear 1; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses