proposition: Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e.
proof: Proof. intros m x; functional induction (find x m); auto; intros; clearf; inv bst; intuition_in; simpl; auto; try solve [order | absurd (X.lt x y); eauto with ordered_type | absurd (X.lt y x); eauto with ordered_type]. Qed.
imports: FunInd FMapInterface FMapList ZArith Int