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