proposition: Lemma find_occ_dec : forall (k : key) (v : data) (d : dict), occ v k (D_tree d) -> find k d = Some v.
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 x0 H0; case (occ_unicity x s _ _ _ H H0). auto. intros. case (n v H). Qed.
imports: Relations List ZArith Arith