I have written a proof using this method.
http://us2.metamath.org:88/downloads/inpreima2.pdfThe references are to metamath. (Not sure they are still up to date.)
http://www.metamath.org/In my opinion, you need a specific editor to write this kind of proof. Writing it
as a latex text in a normal editor is very demanding even with the system of abbreviation
proposed by pf2.
When I was in high school, my main problem (one of my main problems to be honest) was
to deal with all those hypotheses that pop in an out during the proof. Sometimes you could
use them, sometimes you couldn't. With the model of proof proposed here and its hierarchy,
I would have understood.