proposition: Lemma merge_spec1m (f:key->option elt->option elt'->option elt'') : Proper (K.eq==>Logic.eq==>Logic.eq==>Logic.eq) f -> forall (m:t elt)(m':t elt') x, In x m \/ In x m' -> find x (merge f m m') = f x (find x m) (find x m').
proof: Proof. intros Hf m m' x H. now destruct (merge_spec1 f H) as (y,(->,->)). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)