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. induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array. inversion_clear 1; inversion_clear 1; auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance