On a canonical representation for stuck

[YaZko]

With the move to arbitrary branching indexes, stuck is now represented by a certain index B0.
However, we end up injecting B0 into the ambient domain of indexes on a regular basis, and equ is sensible to the specific injection used when working parametrically. This leads to some lemmas being non provable for superficial reasons.

Hardcoding stuckness into a constructor in the structure would resolve the problem.

Edit: I've been a bit quick to despair, care in parametrization of injection instances allows us to sneak around the issue. That remains unfortunate.