proposition: Theorem add_cancel : forall A x v dom (m : t A dom), find x m = Some v -> eq (add x v m) m.
proof: Proof. intros A x v dom m Heq y. destruct (X.eq_dec y x) as [Hxy | Hxy]. + rewrite Hxy, add_same, Heq. reflexivity. + rewrite add_other; trivial. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface