Replace the wp_lb_init lemma with a more general steps_lb_0 lemma which does not depend on WP.
wp_lb_init
steps_lb_0