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. case (occ_inv _ _ _ _ _ _ H2). repeat simple destruct 1. case (occ_inv _ _ _ _ _ _ H3). tauto. simple destruct 1. intro. absurd (occ v' k0 b); auto. eapply not_left. eauto. rewrite H5; apply M.le_refl. intro. absurd (occ v' k0 b0); auto. eapply not_right; eauto. rewrite H5; apply M.le_refl. simple destruct 1; intro. case (occ_inv _ _ _ _ _ _ H3). repeat simple destruct 1. absurd (occ v k b); auto. eapply not_left; eauto. apply M.le_refl. rewrite H7; auto. simple destruct 1; intro. eapply H. eauto with searchtrees. eauto. assumption. absurd (occ v' k0 b0); auto. eapply not_right; eauto with searchtrees. case (maj_l _ _ _ _ H1). intro; apply Key.lt_le_weak. eauto. case (occ_inv _ _ _ _ _ _ H3). repeat simple destruct 1. absurd (occ v k0 b0); auto. case H7. eapply not_right; eauto with searchtrees. apply M.le_refl. simple destruct 1. intro. absurd (occ v' k0 b); auto. eapply not_left; eauto with searchtrees. case (min_r _ _ _ _ H1). intros. apply Key.lt_le_weak. eauto. intro. eapply H0. eauto with searchtrees. eauto. eauto. Qed.
imports: Relations List ZArith Arith