proposition: Lemma add_1 : forall m x y e, eq x y -> MapsTo y e (add x e m).
proof: Proof. intros m x y e; generalize y; clear y. unfold MapsTo. induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1]; simpl; auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance