Substitution

• $x[x:=N]\; ==\; N$
• $y[x:=N]\; ==\; y$ if $x\; !=\; y$
• $(\%l\; y.M)[x:=N]\; ==\; \%l\; y.(M[x:=N])$
• $(M\_1\; M\_2\; )\; [x:=N]$ $==$ $(M\_1\; [x:=N])\; (M\_2[x:=N])$