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.
With the move to arbitrary branching indexes, stuck is now represented by a certain index
B0. However, we end up injectingB0into the ambient domain of indexes on a regular basis, andequis 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.