[runald]

If you had to tediously write it over and over in proofs, why can't just you give it a name or an abstraction?

↑ As you would do in programming.