| 0 | : | nat |
| cons | : | nat → list → list |
| foldl | : | (nat → nat → nat) → nat → list → nat |
| nil | : | list |
| plusc | : | nat → nat → nat |
| s | : | nat → nat |
| sum | : | list → nat |
| F | : | nat → nat → nat |
| Y | : | nat |
| G | : | nat → nat → nat |
| V | : | nat |
| W | : | nat |
| P | : | list |
| X1 | : | nat |
| Y1 | : | nat |
| U1 | : | nat |
| V1 | : | list |
| foldl · (λ%Y:nat.λ%X:nat.F · %Y · %X) · Y · nil | ⇒ | Y |
| foldl · (λ%U:nat.λ%Z:nat.G · %U · %Z) · V · (cons · W · P) | ⇒ | foldl · (λ%W:nat.λ%V:nat.G · %W · %V) · (G · V · W) · P |
| plusc · X1 · 0 | ⇒ | X1 |
| plusc · Y1 · (s · U1) | ⇒ | s · (plusc · Y1 · U1) |
| sum · V1 | ⇒ | foldl · (λ%G:nat.λ%F:nat.plusc · %G · %F) · 0 · V1 |