proposition: Lemma map2_bst : forall m m', bst m -> bst m' -> bst (map2 f m m').
proof: Proof. unfold map2; intros. apply map2_opt_bst with (fun _ => f); auto using map_option_bst; intros; rewrite map_option_find; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int