proposition: Theorem empty_def : forall k : key, find k empty = None.
proof: Proof. unfold find, empty in |- *. intro k; case (occ_dec k leaf leaf_search_tree); simpl in |- *. simple destruct s. inversion 1. auto. Qed.
imports: Relations List ZArith Arith