proposition: Lemma occ_unicity : forall t:btree, search_tree t -> forall (k:key) (v v':data), occ v k t -> occ v' k t -> v = v'.
proof: Proof. simple induction t. - inversion 2. - intros k d b H b0 H0 H1 k0 v v' H2 H3; case (occ_inv _ _ _ _ _ _ H2); case (occ_inv _ _ _ _ _ _ H3). + intuition; congruence. + destruct 1; destruct 1. * subst k0 v; absurd (occ v' k b); auto. eapply not_left; eauto; apply M.le_refl. * subst k0 v; absurd (occ v' k b0); auto. eapply not_right; eauto; apply M.le_refl. + destruct 1;intros; subst k0 v'. * destruct H6;auto. absurd (occ v k b); auto. eapply not_left; eauto. apply M.le_refl. absurd (occ v k b0); auto. eapply not_right; eauto. apply M.le_refl. + destruct 1. * destruct 1. apply H with k0; eauto. inversion H1;auto. destruct (left_right_not_compat _ _ _ _ _ _ _ H1 H4 H5). * destruct 1. destruct (left_right_not_compat _ _ _ _ _ _ _ H1 H5 H4). eapply H0;eauto. inversion H1;auto. Qed.
imports: Relations List ZArith Arith