proposition: Theorem map_None : forall A B (f : A -> B) dom (m : t A dom) x, find x (map f m) = None <-> ¬Dom.In x dom.
proof: Proof. intros A B f dom m x. rewrite <- (find_spec x m). split; intro Hin. + intros [v Hv]. assert (Hconj : exists v', find x m = Some v' ∧ f v' = f v) by now exists v; split. rewrite <- map_spec in Hconj. rewrite Hconj in Hin. discriminate Hin. + destruct (find x (map f m)) eqn:Hmap; trivial. elim Hin. rewrite map_spec in Hmap. destruct Hmap as [v [Hv _]]. exists v. assumption. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface