| append | : | [b × b] ⟶ b |
| cons | : | [a × b] ⟶ b |
| map | : | [a → a × b] ⟶ b |
| nil | : | b |
| X | : | b |
| Y | : | a |
| U | : | b |
| V | : | b |
| I | : | a → a |
| J | : | a → a |
| X1 | : | a |
| Y1 | : | b |
| U1 | : | b |
| V1 | : | b |
| W1 | : | b |
| J1 | : | a → a |
| X2 | : | b |
| Y2 | : | b |
| append(nil, X) | ⇒ | X |
| append(cons(Y, V), U) | ⇒ | cons(Y, append(V, U)) |
| map(I, nil) | ⇒ | nil |
| map(J, cons(X1, Y1)) | ⇒ | cons(J · X1, map(J, Y1)) |
| append(append(U1, V1), W1) | ⇒ | append(U1, append(V1, W1)) |
| map(J1, append(X2, Y2)) | ⇒ | append(map(J1, X2), map(J1, Y2)) |