proposition: Lemma map_option_find : forall (m:t elt)(x:key), bst m -> find x (map_option f m) = match (find x m) with Some d => f x d | None => None end.
proof: Proof. intros m; functional induction (map_option f m); simpl; auto; intros; inv bst; rewrite join_find || rewrite concat_find; auto; simpl; try destruct X.compare as [Hlt|Heq|Hlt]; simpl; auto. - rewrite (f_compat d Heq); auto. - intros y H; destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. - intros y H; destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. - rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto. - rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto. rewrite (f_compat d Heq); auto. - rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto. destruct (find x0 (map_option f r)); auto. - intros y y' H H'. destruct (map_option_2 H) as (? & ? & ?). destruct (map_option_2 H') as (? & ? & ?). eapply X.lt_trans with x; eauto using MapsTo_In. Qed.
imports: FunInd FMapInterface FMapList ZArith Int