proposition: Lemma add_2 : forall m x y e e', ~ eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
proof: Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e0];simpl;auto with smtcoq_array; clear e0. subst;auto with smtcoq_array. intros y' e'' eqky'; inversion_clear 1; destruct H0; simpl in *. subst. now contradict eqky'. auto with smtcoq_array. auto with smtcoq_array. intros y' e'' eqky'; inversion_clear 1; intuition. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance