cleaned up lots of FIXMEs in ProofToLatex