The idea was to flatten the structured traces and show that these are the same
as the original trace. This looks like it could work out OK, but with the
caveats that:
1. flattening is a not-quite trivial operations - we need to define a type
of finite flat traces to get out of the finite structured traces, get the
executable parts from Prop into Type[0] using their executability, then
define a careful pair of mutual cofixpoints to satisfy the guardedness
conditions;
2. we can't show the usual equality on coinductive data, so we need to define
a specialised coinductive equality predicate for flat traces; and
3. define a cofixpoint proof for that tediously going through all of the
structure I defined at 1 (this is the point that I'm at).
After all of this, we get a corrollary saying the the flattened result of
making a structured trace must be the same as the original trace because all
traces from the same place are.