I think I get the substitution notation in lambda calculus for "simple" applications such as:
What I don't get is how that works when I pass a lambda as the "parameter". E.g. to compose functions
This clearly makes no sense. What does it mean to multiply an abstraction by 2?
I "understand" that the above is meant to yield:
But I can't see how strictly following the substitution algorithm allows one to arrive at that result.