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; cbn in |- *; intros. case (occ_dec k x s); cbn in |- *. - simple destruct s0; cbn in |- *; intros x0 H0; case (occ_unicity x s _ _ _ H H0); auto. - intro; case (n v H). Qed.
imports: Relations List ZArith Arith