proposition: Theorem to_btree_inb : forall a b, inpb (pbleaf a) b -> inb (leaf a) (to_btree b).
proof: Proof. intros a b; generalize a; elim b; clear a b; simpl in |- *; auto. intros a a0 H; inversion H; auto. intros p H a H0; apply H; auto; inversion H0; auto. intros p H a H0; apply H; auto; inversion H0; auto. intros p H p0 H0 a H1; inversion H1; auto. Qed.