WIP, but that is the target ethos in the prover I'm building:

https://github.com/ityonemo/bpa

Its painfully verbose and explicit but its designed to let you cut down to the structure of the proof with a query language