This relies on #3, however, once Monaco is implemented, it should be pretty doable to collapse subproofs using the little arrows on the left. When collapsed a proof should show the premises and the conclusion (or perhaps just the conclusion?)
