proposition: Lemma merge_spec2 m m' x {Hm:Ok m}{Hm':Ok m'} : In x (merge m m') -> In x m \/ In x m'.
proof: Proof. rewrite <- domains_InA; trivial. intros (e,H). red in H. rewrite InA_alt in H. destruct H as ((k,e'),(E,H)). unfold merge in H; rewrite fold_keys_In in H. destruct H as (H,_). apply InA_alt. exists k. split; trivial. now destruct E. Qed.
imports: Coq(EqualitiesFacts)