proposition: Theorem add_incl : forall A x v dom (m : t A dom), ¬Dom.In x dom -> incl m (add x v m).
proof: Proof. intros A x v dom m Hdom y v' Hin. rewrite add_other; trivial. intro Habs. apply Hdom. rewrite <- Habs, <- find_spec. exists v'. eassumption. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface