To build the non-terminating structural traces we need to do more than just
write a function that mirrors the structure of the resulting data type.
To know which (coinductive) constructor to use we must first examine the
trace to find whether we encounter a label or a non-terminating function
next (terminating function calls will be buried in the finite part of the
trace).
It should be possible to implement this process with a terminating function
using the fact that the program is well-labelled (i.e., it isn't possible to
spend an infinite amount of time in one function because you'll encounter a
label).
However, the current well-labelled predicate is given in purely syntactic
terms: it requires the successors of branching instructions to be labels.
This was sufficient for the finite traces because we already knew that they
are terminating. I will need to construct an additional criterion to catch
loops and show that the traces enjoy it.