Substitution in untyped Lambda calculus is complicated by variable capture.
Can this boring technical complication be entirely avoided by some restriction on the standard formation rules? Something that prevents the dangerous symbol duplication. If so, how? Otherwise why not?
Alternatively, can the complication be avoided by uniformly alpha-converting every Lambda abstraction of the final composite, to ensure that every binding/bound variable symbol only appears locally (and therefore never as a free variable in the argument of an application term). If so, it seems that the substitution rules could be simplified.