proposition: Lemma map2_2 {elt elt' elt''}(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt'') : In x (map2 f m m') -> In x m \/ In x m'.
proof: Proof. apply merge_spec2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)