proposition: Lemma map2_1 {elt elt' elt''}(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt'') : In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m').
proof: Proof. intros. unfold map2. now destruct (merge_spec1 (fun _ => f) H) as (y,(_,->)). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)