tweak adequacy: treat stuckness like the other WP indices

Seems inconsistent to single out this one index as something that is fixed together with the execution trace. And this doesn't make the theorem any harder to use in Coq either.