proposition: Lemma map2_1 : forall (elt elt' elt'':Type)(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 elt elt' elt'' m m' x f; exact (@Raw.map2_1 elt elt' elt'' f (this m) (sorted m) (this m') (sorted m') x). Qed.
imports: FMapInterface