proposition: Remark success2 : forall (d : dict) (k : key) (v : data), occ v k (D_tree (add k v d)).
proof: Proof. simple destruct d. simpl in |- *. intros x s k v; case (insert k v x s); simpl in |- *. simple destruct 1. eauto with searchtrees. Qed.
imports: Relations List ZArith Arith