It depends on whether or not the buyer allows for proof irrelevance. There are cases where _human_ buyers care about the structure of the proof. In particular,

It depends on whether or not the buyer allows for proof irrelevance. There are cases where _human_ buyers care about the structure of the proof. In particular, just like with code, you'd prefer a proof that is maintainable, modular, and not-too-hard to update if your assumptions or claim changes.