Alphabet

f:a → b → c
f1:[a] ⟶ b → c
f2:[a × b] ⟶ c

Variables

x:a
y:b

Rules

f1(x)f · x
f2(x, y)f1(x) · y