Alphabet

nil:listf
cons:[a → a × listf] ⟶ listf
dapply:[a × a → a × a → a] ⟶ a
lapply:[a × listf] ⟶ a

Variables

x:a
F:a → a
G:a → a
lf:listf

Rules

dapply(x, F, G)⇒F · (G · x)
lapply(x, nil)⇒x
lapply(x, cons(F, lf))⇒F · lapply(x, lf)