A subproof is a type of shell that has no title on top and no other special functionality. It can be used inside proofs to group collections of subderivations together, but without adding the unnecessary (and confusing) heading "Proof" on top of them, which would be the case if we were instead to use the Proof class.