proposition: Lemma domains_InA m m' (Hm : Ok m) x : InA K.eq x (domains m m') <-> In x m \/ In x m'.
proof: Proof. unfold domains. assert (Proper (K.eq==>eq) (restrict m)). { intros k k' Hk. unfold restrict. now rewrite (find_eq Hm Hk). } rewrite InA_app_iff, filter_InA, !mapfst_InA; intuition. unfold restrict. destruct (find x m) eqn:F. - left. apply find_spec in F; trivial. now exists e. - now right. Qed.
imports: Coq(EqualitiesFacts)