Replace TrPred and t+ with t++

[sctfn]

The reference from which I derived TrPred has been rewritten so I no longer have a reference for it. In general, the preference in the literature is to define the transitive closure of a relationship instead of the transitive predecessors. This would imply using t+, except that I need to use this on proper classes. I found an appropriate definition in Levy and have added it to my mathbox as t++. This issue is to discuss moving t++ into main.

The steps I'm planning on taking are:

1. Move t++ to main
2. Fix up well-founded induction
3. Fix up well-founded recursion
4. Remove TrPred
5. Replace t+ in main
6. Maybe go in to t+ in mathboxes

The first bit of this is in #4454