proposition: Theorem add_None : forall A x y v dom (m : t A dom), find y (add x v m) = None <-> ¬X.eq y x ∧ find y m = None.
proof: Proof. intros A x y v dom m. destruct (X.eq_dec y x) as [Hxy | Hxy]. + rewrite Hxy, add_same. split; intro Hin. - discriminate Hin. - destruct Hin as [Hin _]. now elim Hin. + rewrite add_other; trivial. intuition. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface