proposition: Lemma map_option_bst : forall m, bst m -> bst (map_option f m).
proof: Proof. intros m; functional induction (map_option f m); simpl; auto; intros; inv bst. - apply join_bst; auto; intros y H; destruct (map_option_2 H) as (d0 & ? & ?); eauto using MapsTo_In. - apply concat_bst; auto; intros y y' H H'. destruct (map_option_2 H) as (d0 & ? & ?). destruct (map_option_2 H') as (d0' & ? & ?). eapply X.lt_trans with x; eauto using MapsTo_In. Qed.
imports: FunInd FMapInterface FMapList ZArith Int