Extend the flag derivation of Exercise 5.2(b) to a complete derivation of
$$S : *, Q : S →S →* ⊢ Πx : S. Πy : S. Qxy : *$$
The following is the flag derivation (click to enlarge).
