proposition: Lemma rm_5 : forall p0:Z, occ p0 (Z_bnode n (Z_bnode p t1 t2) t') -> occ p0 (Z_bnode q t0 t') \/ n = p0.
proof: Proof. intros p0 H; case (occ_inv H). - intro e ; elim e; auto with searchtrees. - intro H1; case H1; intro H'1. + elim R; intros H2 H3 H4 H5 H6 H7; elim (H5 p0 H'1); left; auto with searchtrees. subst p0; auto with searchtrees. + left; auto with searchtrees. Qed.
imports: ZArith Extraction List