| abs | : | (a → a) → aa |
| app | : | aa → a → a |
| let | : | ta → (a → ta) → ta |
| return | : | a → ta |
| F | : | a → a |
| Y | : | a |
| U | : | aa |
| V | : | a |
| I | : | a → ta |
| P | : | ta |
| X1 | : | ta |
| Z1 | : | a → ta |
| G1 | : | a → ta |
| app · (abs · (λ%X:a.F · %X)) · Y | ⇒ | F · Y |
| abs · (λ%Y:a.app · U · %Y) | ⇒ | U |
| let · (return · V) · (λ%Z:a.I · %Z) | ⇒ | I · V |
| let · P · (λ%U:a.return · %U) | ⇒ | P |
| let · (let · X1 · (λ%W:a.Z1 · %W)) · (λ%V:a.G1 · %V) | ⇒ | let · X1 · (λ%G:a.let · (Z1 · %G) · (λ%F:a.G1 · %F)) |