| 0 | : | nat |
| cons | : | nat → list → list |
| foldr | : | (nat → nat → nat) → nat → list → nat |
| length | : | list → nat |
| nil | : | list |
| s | : | nat → nat |
| F | : | nat → nat → nat |
| Y | : | nat |
| G | : | nat → nat → nat |
| V | : | nat |
| W | : | nat |
| P | : | list |
| X1 | : | list |
| foldr · (λ%Y:nat.λ%X:nat.F · %Y · %X) · Y · nil | ⇒ | Y |
| foldr · (λ%U:nat.λ%Z:nat.G · %U · %Z) · V · (cons · W · P) | ⇒ | G · W · (foldr · (λ%W:nat.λ%V:nat.G · %W · %V) · V · P) |
| length · X1 | ⇒ | foldr · (λ%G:nat.λ%F:nat.s · %F) · 0 · X1 |