proposition: Lemma find_in_equiv : forall m m' x, bst m -> bst m' -> find x m = find x m' -> (In x m <-> In x m').
proof: Proof. split; intros; apply find_in; [ rewrite <- H1 | rewrite H1 ]; apply in_find; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int