(λx. t) u ↪ t[u/x]