proposition: Lemma add_1 : forall m x y e, e <> m.(default) -> eq x y -> MapsTo y e (add x e m).
proof: Proof. intros. unfold add, raw_add_nodefault. unfold MapsTo. simpl. case_eq (cmp e m.(default)); intro; auto. unfold cmp in H1. destruct (compare e m.(default)); try now contradict H1. apply Raw.add_1; auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance