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