Alphabet
c
:
((C → L) → L) → C
d
:
C
ex
:
C → L
nil
:
L
Variables
F
:
(C → L) → L
Rules
ex
·
d
⇒
nil
ex
· (
c
· (λ
%X
:C -> L.
F
·
%X
))
⇒
F
·
ex