Generalize wp_lb_init to steps_lb_0.
Replace the wp_lb_init
lemma with a more general steps_lb_0
lemma which does not depend on WP.
Edited by Ralf Jung
Replace the wp_lb_init
lemma with a more general steps_lb_0
lemma which does not depend on WP.