I'm studying "A simple proof of a theorem of Statman" by H.G. Mairson.
At page 4, he encodes set/type theory in lambda calculus. In particular, note che "op" trick in the definition of $eq_{k+1}$.
Mairson stress the fact that this trick is essential, because writing $subset_{k+1}$ twice would cause exponential blowup in term size. I'm asking why! That would not just double the term size?