proposition: Remark diff_key2 : forall (d : dict) (k k' : key) (v v' : data), k <> k' -> occ v k (D_tree d) -> occ v k (D_tree (add k' v' d)).
proof: Proof. simple destruct d; simpl in |- *. intros x s k k' v v'; case (insert k' v' x s); simpl in |- *. simple destruct 1; intros. case (H _ _ H4). intro H5; case (H3 H5). auto. Qed.
imports: Relations List ZArith Arith