In the proof transformation mode it would be very helpful if the cut formula in each premiss of a cut rule were somehow distinguished (either with a marker, or with a different colour, or a typographic hint).
Otherwise, due to implicit exchanges it becomes quite difficult to track which is cut againts which.
In the proof transformation mode it would be very helpful if the cut formula in each premiss of a cut rule were somehow distinguished (either with a marker, or with a different colour, or a typographic hint).
Otherwise, due to implicit exchanges it becomes quite difficult to track which is cut againts which.