Exponential blowup in Simple Proof of a theorem of Statman by Mairson 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?
Ok, I think I've got it.

$eq_{k+1}$ calls (indirectly) $eq_k$, so, if I call $subset_{k+1}$ twice, I fall in an exponential blowup because of the two recursive calls of $eq_k$: it is simple to see with a "linear recurrence relation of constant order".