| app | : | arrAB → A → B |
| case | : | SAB → (A → C) → (B → C) → C |
| inl | : | A → SAB |
| inr | : | B → SAB |
| lam | : | (A → B) → arrAB |
| F | : | A → B |
| Y | : | A |
| U | : | arrAB |
| V | : | A |
| I | : | A → C |
| J | : | B → C |
| X1 | : | B |
| Z1 | : | A → C |
| G1 | : | B → C |
| app · (lam · (λ%X:A.F · %X)) · Y | ⇒ | F · Y |
| lam · (λ%Y:A.app · U · %Y) | ⇒ | U |
| case · (inl · V) · (λ%U:A.I · %U) · (λ%Z:B.J · %Z) | ⇒ | I · V |
| case · (inr · X1) · (λ%W:A.Z1 · %W) · (λ%V:B.G1 · %V) | ⇒ | G1 · X1 |