Alphabet

cons:[c × d] ⟶ d
fcons:[b → c × a] ⟶ a
fmap:[a × b] ⟶ d
fnil:a
nil:d

Variables

X:b
Z:b → c
U:a
V:b

Rules

fmap(fnil, X)⇒nil
fmap(fcons(Z, U), V)⇒cons(Z · V, fmap(U, V))