| bind | : | Ta → (a → Ta) → Ta |
| return | : | a → Ta |
| X | : | a |
| Z | : | a → Ta |
| U | : | Ta |
| V | : | Ta |
| I | : | a → Ta |
| J | : | a → Ta |
| bind · (return · X) · (λ%X:a.Z · %X) | ⇒ | Z · X |
| bind · U · (λ%Y:a.return · %Y) | ⇒ | U |
| bind · (bind · V · (λ%U:a.I · %U)) · (λ%Z:a.J · %Z) | ⇒ | bind · V · (λ%W:a.bind · (I · %W) · (λ%V:a.J · %V)) |