Exercise 4.3
(a) Give a complete (i.e. not shortened) λω-derivation in flag format of
$$α,β : ∗, x : α, y : α →β ⊢ yx : β$$
(b) Give a shortened λω-derivation in flag format of
$$α,β : ∗, x : α, y : α →β, z : β →α ⊢ z(yx) : α$$
(a) The flag notation derivation is as follows (click to enlarge).
(b) The flag notation derivation is as follows (click to enlarge). It expands on the above because all except one statement in the context is the same as the previous example.
