| cons | : | a → alist → alist |
| map | : | (a → a) → alist → alist |
| nil | : | alist |
| o | : | (a → a) → (a → a) → a → a |
| F | : | a → a |
| Z | : | a → a |
| U | : | a |
| V | : | alist |
| I | : | a → a |
| J | : | a → a |
| X1 | : | alist |
| Z1 | : | a → a |
| G1 | : | a → a |
| V1 | : | a |
| map · (λ%X:a.F · %X) · nil | ⇒ | nil |
| map · (λ%Y:a.Z · %Y) · (cons · U · V) | ⇒ | cons · (Z · U) · (map · (λ%Z:a.Z · %Z) · V) |
| map · (λ%V:a.I · %V) · (map · (λ%U:a.J · %U) · X1) | ⇒ | map · (λ%W:a.o · (λ%G:a.I · %G) · (λ%F:a.J · %F) · %W) · X1 |
| o · (λ%I:a.Z1 · %I) · (λ%H:a.G1 · %H) · V1 | ⇒ | Z1 · (G1 · V1) |