proposition: Lemma not_find_occ_dec : forall (k : key) (d : dict), (forall v : data, ~ occ v k (D_tree d)) -> find k d = None.
proof: Proof. unfold find in |- *; simple destruct d; simpl in |- *; intros. case (occ_dec k x s); simpl in |- *. simple destruct s0; simpl in |- *. intros. case (H _ o). auto. Qed.
imports: Relations List ZArith Arith