| cons | : | a → alist → alist |
| foldl | : | (a → a → a) → a → alist → a |
| nil | : | alist |
| F | : | a → a → a |
| Y | : | a |
| G | : | a → a → a |
| V | : | a |
| W | : | a |
| P | : | alist |
| foldl · (λ%Y:a.λ%X:a.F · %Y · %X) · Y · nil | ⇒ | Y |
| foldl · (λ%U:a.λ%Z:a.G · %U · %Z) · V · (cons · W · P) | ⇒ | foldl · (λ%W:a.λ%V:a.G · %W · %V) · (G · V · W) · P |