I have three mutually recursive functions for building the structured traces
from flat RTLabs traces for a terminating function. The guardedness check for
these fails for two reasons:
1. some of the uses of the other functions pass the "decreasing" argument
(the termination proof) without making it smaller, because the "real"
processing happens in another function; and
2. recursive calls consume a prefix of the termination proof and the
remainder is returned for building more of the structured trace, but
matita doesn't know that this is smaller than the original argument.
Both of these could be solved at the same time if I produce a termination
counter together with a proof that it is at least as large as 3 times the
length of the termination proof.
For now I've put the termination definition into Type[0] rather than Prop
so that I can define the length function. This might cause trouble when
applying the excluded middle, but I'll worry about that later.