local f = Const("f")
assert(f:size() == 1)
local x = Var(0)
assert(x:size() == 1)
assert(f(x):size() == 3)
local t = f(x)
assert(t(x):size() == 4)
assert(t(x)(f(x)):size() == 7)
assert(mk_lambda("x", Const("Nat"), f(x)):size() == 5)