proposition: Lemma merge_spec1 m m' x {Hm:Ok m}{Hm':Ok m'} : In x m \/ In x m' -> exists y:key, K.eq y x /\ find x (merge m m') = f y (find x m) (find x m').
proof: Proof. assert (Hmm' : Ok (merge m m')) by now apply merge_ok. rewrite <- domains_InA; trivial. rewrite InA_alt. intros (y,(Hy,H)). exists y; split; [easy|]. rewrite (find_eq Hm Hy), (find_eq Hm' Hy). destruct (f y (find y m) (find y m')) eqn:F. - apply find_spec; trivial. red. apply InA_alt. exists (y,e). split. now split. unfold merge. apply fold_keys_In. now split. - destruct (find x (merge m m')) eqn:F'; trivial. rewrite <- F; clear F. symmetry. apply find_spec in F'; trivial. red in F'. rewrite InA_alt in F'. destruct F' as ((y',e'),(E,F')). unfold merge in F'; rewrite fold_keys_In in F'. destruct F' as (H',F'). compute in E; destruct E as (Hy',<-). replace y with y'; trivial. apply (@NoDupA_unique_repr (domains m m')); auto. now apply domains_ok. now transitivity x. Qed.
imports: Coq(EqualitiesFacts)