Parser can be optimized further by separating pretty-print and tree construction into two different stages

[antonkov]

Each MVarId is now printed at least twice - once in goalsBefore and once in goalsAfter (sometimes unnecessary even more from parent nodes when it already handled in the subtree - and then it's also discarded). Profiling shows that pretty printing takes ~90% on big proofs. By separating {MVarId => GoalInfo} mapping from ProofSteps we could cheaply optimize parser ~x2