proposition: Lemma merge_spec1 {elt elt' elt''} (f:key->option elt->option elt'->option elt'') m m' x : In x m \/ In x m' -> exists y:key, K.eq y x /\ find x (merge f m m') = f y (find x m) (find x m').
proof: Proof. apply merge_spec1; apply ok. Qed.