proposition: Lemma domains_ok m m' : NoDupA eqk m -> NoDupA eqk m' -> NoDupA K.eq (domains m m').
proof: Proof. intros Hm Hm'. unfold domains. apply NoDupA_app; auto with *. - now apply mapfst_ok. - now apply list_filter_ok, mapfst_ok. - intros x. rewrite mapfst_InA. intros (e,H). apply find_spec in H; trivial. rewrite InA_alt. intros (y,(Hy,H')). rewrite (find_eq Hm Hy) in H. rewrite filter_In in H'. destruct H' as (_,H'). unfold restrict in H'. now rewrite H in H'. Qed.
imports: Coq(EqualitiesFacts)