About to make reduction proof-relevant so I can define the refinement map on traces.
Split proof-relevant and irrelevent terms. The relation still needs work.