proposition: Remark diff_key1 : forall (d : dict) (k k' : key) (v v' : data), k <> k' -> occ v k (D_tree (add k' v' d)) -> occ v k (D_tree 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 (H1 _ _ H4). auto. simple destruct 1; absurd (k' = k); auto. case H5; auto. Qed.
imports: Relations List ZArith Arith