proposition: Lemma map2_1 : forall m m' y, bst m -> bst m' -> In y m \/ In y m' -> find y (map2 f m m') = f (find y m) (find y m').
proof: Proof. unfold map2; intros. rewrite (map2_opt_1 (f0:=fun _ => f)); auto using map_option_bst; intros; rewrite map_option_find; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int