| abs | : | (a → b) → ab |
| app | : | ab → a → b |
| appBG | : | BGaBGb → BGa → BGb |
| banga | : | a → BGa |
| let | : | BGa → (a → BGb) → BGb |
| F | : | a → b |
| Y | : | a |
| U | : | ab |
| V | : | a |
| I | : | a → BGb |
| P | : | BGa |
| X1 | : | BGaBGb |
| app · (abs · (λ%X:a.F · %X)) · Y | ⇒ | F · Y |
| abs · (λ%Y:a.app · U · %Y) | ⇒ | U |
| let · (banga · V) · (λ%Z:a.I · %Z) | ⇒ | I · V |
| let · P · (λ%U:a.appBG · X1 · (banga · %U)) | ⇒ | appBG · X1 · P |