fact: Parameter merge_spec1 : forall (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').
imports: MMaps(Comparisons)