Proof of ball_respects_bsublist