Enhancement: implement `Fix.cases` such that an entire recursion of the data structure is not required

[Equilibris]

Currently, we implement cases using the recursor. This means every time we want to do a cases operation we have to walk the entire datastructure just to throw away the result at the end.
This is fine for proving, but might not be good for computation.

It might be possible to use Fix.dest, which effectively unfolds a fixpoint type once,
but it turns out that Fix.dest is implemented using Fix.drec, so this would not avoid the full recursion.

In future it might be worth fixing this by adding the correct theorems to dest and removing its dependence on rec.