proposition: Theorem to_btree_inpb : forall a b, inb (leaf a) (to_btree b) -> inpb (pbleaf a) 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 p0 H0 a H1. inversion H1; auto. Qed.