| 0 | : | nat |
| cons | : | nat → natlist → natlist |
| foldl | : | (nat → nat → nat) → nat → natlist → nat |
| nil | : | natlist |
| plus | : | nat → nat → nat |
| sum | : | natlist → nat |
| F | : | nat → nat → nat |
| Y | : | nat |
| G | : | nat → nat → nat |
| V | : | nat |
| W | : | nat |
| P | : | natlist |
| X1 | : | natlist |
| 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 |
| sum · X1 | ⇒ | foldl · (λ%G:nat.λ%F:nat.plus · %G · %F) · 0 · X1 |