Exponential blowup in Simple Proof of a theorem of Statman by Mairson

Question

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?

Answer 1

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".