Alphabet
f
:
[A → B] ⟶ B
a
:
B
b
:
B
c
:
B
Variables
Rules
f
(λ
x
:A.
a
)
⇒
b
b
⇒
f
(λ
x
:A.
c
)