Alphabet
abs
:
(a → b) → Arrab
app
:
Arrab → a → b
box
:
a → Boxa
unbox
:
Boxa → a
Variables
F
:
a → b
Y
:
a
U
:
Arrab
V
:
a
W
:
Boxa
Rules
app
· (
abs
· (λ
%X
:a.
F
·
%X
)) ·
Y
⇒
F
·
Y
abs
· (λ
%Y
:a.
app
·
U
·
%Y
)
⇒
U
unbox
· (
box
·
V
)
⇒
V
box
· (
unbox
·
W
)
⇒
W