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); cbn in |- *. - simple destruct s; inversion 1. - reflexivity. Qed.
imports: Relations List ZArith Arith