Alphabet
fapp
:
[o × o] ⟶ o
lam
:
[o → o] ⟶ o
Variables
X
:
o → o
Y
:
o
Rules
fapp
(
lam
(
X
),
Y
)
⇒
X
·
Y