proposition: Lemma add_1 : forall m x y e, e <> default_value -> eq x y -> MapsTo y e (add x e m).
proof: Proof. intros m x y e H H0. unfold add, raw_add_nodefault. unfold MapsTo. simpl. case_eq (cmp e default_value); intro H1; auto. - elim H. unfold cmp in H1. now rewrite compare2eqb_spec in H1. - apply Raw.add_1; auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance