Include TraceCheck proofs, make TraceCheckParser able to hande non left-associative proofs, include TraceCheck into CLI