Fixtype of semantic proof list outcomes.
This is a tagged union type, introduced by fty::deftagsum.
These are the possible results of checking a list of proof trees in turn. If any tree yields an error or a failure, that is also the outcome. Otherwise, all the trees yield assertions, so the outcome is a list of assertions.