Alphabet
f
:
[o → o] ⟶ o
g
:
o → o
Variables
Rules
f
(
g
)
⇒
f
(λ
%X
:o.
g
·
%X
)