proposition: Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true.
proof: Proof. intros m x; functional induction (mem x m); auto; intros; clearf; inv bst; intuition_in; order. Qed.
imports: FunInd FMapInterface FMapList ZArith Int