Alphabet
app
:
arrab → a → b
lam
:
(a → b) → arrab
Variables
F
:
a → b
Y
:
a
U
:
arrab
Rules
app
· (
lam
· (λ
%X
:a.
F
·
%X
)) ·
Y
⇒
F
·
Y
lam
· (λ
%Y
:a.
app
·
U
·
%Y
)
⇒
U