lambda calculus example - DukeDrake

lc.txt

(\g.\f.\x. g f (f x)) (\f.\x. x)

(\g. \f0. \x0. g f0 (f0 x0)) (\f1. \x1. x1) -- alpha rename to avoid collisions

\f0. \x0. (\f1. \x1. x1) f0 (f0 x0) -- apply parameter for g
    g = (\f1. \x1. x1)

\f0. \x0. f0 x0 -- apply parameters to inner lambda and reduce
    f1 = f0
    x1 = f0 x0
    reduction of (\f1. \x1. x1) eliminates f1 and produces x1

one can now further note that the above is essentially id, because it takes
  f0 x0 and produces f0 x0