Alphabet
f
:
a → b → c
f1
:
[a] ⟶ b → c
f2
:
[a × b] ⟶ c
Variables
x
:
a
y
:
b
Rules
f
·
x
⇒
f1
(
x
)
f1
(
x
) ·
y
⇒
f2
(
x
,
y
)