More thesis hacking. Another big hole found and (I think) patched. I needed a vastly more algorithmic proof of M1 o M = M2 o M implies M1 = M2.