Exercise 2.9
Give derivations by means of which the following judgements become type-checked. You may use the flag notation. In part (b), you may use flag notation in its ‘shortened’ form, i.e. suppress steps involving the (var)-rule.
(a) $x : δ→δ→α, y : γ→α, z : α→β ⊢ λu : δ. λv : γ. z(yv) : δ →γ →β$
(b) $x : δ→δ→α, y : γ→α, z : α→β ⊢ λu : δ. λv : γ. z(xuu) : δ →γ →β$
(a) The following flag notation proof confirms the judgement is type-checked (click to enlarge).
(b) The following flag notation proof confirms the judgement is type-checked.
