Fix a few bugs due to wrong information in justification

Currently justification is a function returning Protected<goalstate0>.

Therefore, there are some wrong values which could be pumped into
justification and they emerge in proving phase, not in backtracking
phase (using ORELSE).

To fix those, we have to ensure that inputs are well-formed (those are
not exceptions).

There is a bug in ITAUT_TAC causing too-deep recursion. We limit to
10000 runs for now.

Some bugs e.g. one in EQ_TRANS have been fixed.

Currently there are 114 failures until the one in pair module.
Change Protected<thm0> list to thm0 list in declaration of justification

It will rule out the possibility of passing exceptions to arguments