rewrite bfs proof without eelim hackery; stronger end goal