Comment by ndriscoll

Proofs are not nice and modular though unless they can be extracted into a macro/tactic (or theorem), which I said belongs. They are literally not reusable. The perspective I'm coming from is that we should extract what is valuable as elevated theorems, leaving only the not-so-valuable technical details as the proofs. The connections between objects are theorems.