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. induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac end. inversion_clear 3; auto with smtcoq_array. compute in H1; destruct H1. subst; now contradict H. inversion_clear 1; inversion_clear 2; auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance