• x[x:=N] ≡ N

  • y[x:=N] ≡ y if x ≠ y

  • (λy.M)[x:=N] ≡ λy.(M[x:=N])

  • (M1 M2 ) [x:=N] ≡    (M1 [x:=N]) (M2[x:=N])

slide: The lambda calculus -- substitution