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.
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.