Alphabet
f
:
[o × o] ⟶ o
g
:
o → o → o
a
:
o
b
:
o
Variables
F
:
o → o
G
:
o → o
Rules
f
((λ
z
:o.
F
·
z
) ·
a
,
G
·
a
)
⇒
g
· (
F
·
b
) · (
G
· (
F
·
b
))