proposition: Lemma add_3 : forall m x y e e', ~ eq x y -> MapsTo y e (add x e' m) -> MapsTo y 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 e1];simpl; intros. apply (In_inv_3 H0); compute; auto with smtcoq_array. apply (In_inv_3 H0); compute; auto with smtcoq_array. constructor 2; apply (In_inv_3 H0); compute; auto with smtcoq_array. inversion_clear H0; auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance