In my opinion, you need a specific editor to write it. Writing it
as a latex text in a normal editor is very demanding even with the system of abbreviation
proposed by pf2.
The main problem with this kind of proof is that the hierarchy of sublevels can be very deep and
it's hard to write it on a sheet of paper. But you can make a reference to another sheet of paper obviously.
--
FL