Producing the structured trace for a non-terminating function requires
building some finite sections.  Depending on whether the next "interesting"
state in a non-terminating is a label or a call to a non-terminating function
we need to construct a [trace_label_label] or a [trace_label_call],
corresponding to the [tld_step] and [tld_base] constructors.

So we walk forward through the trace (recursing on the witness to the fact
that the trace is "soundly labelled") and

  - if we encounter a labelled state start returning, building a
    [trace_label_label] as we go (it would be nice to use the existing
    function, but that would probably be more rather than less work;

  - if we encounter a function call ask the excluded middle whether the call
    will terminate; if it does then recurse and use [make_label_return] to
    build the trace_label_return that whatever result will require, if it
    doesn't then start return a [trace_label_call] (via a [trace_any_call]);

  - otherwise just recurse, then add the appropriate step to whichever type of
    trace is returned.