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. unfold add, raw_add_nodefault, MapsTo. simpl. intros m x y e e'. case_eq (cmp e' default_value); intro; auto. case_eq (Raw.mem key_comp x m); intro; auto. intro. apply (Raw.remove_3 _ m.(sorted)); auto. apply Raw.add_3; auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance