Alphabet
New
:
(N → A) → A
Variables
X
:
A
Z
:
N → N → A
Rules
New
· (λ
%X
:N.
X
)
⇒
X
New
· (λ
%Z
:N.
New
· (λ
%Y
:N.
Z
·
%Z
·
%Y
))
⇒
New
· (λ
%U
:N.
New
· (λ
%V
:N.
Z
·
%V
·
%U
))