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; cbn in |- *; intros x s; case (occ_dec k x s); cbn in |- *. - simple destruct s0; simpl in |- *; intros x0 o H; case (H _ o). - reflexivity. Qed.
imports: Relations List ZArith Arith