I'm a bit stuck in Geuvers' "Introduction to Type Theory" (http://www.cs.ru.nl/~herman/onderwijs/provingwithCA/paper-lncs.pdf), p. 39:
Exercise 13. Prove the derivability of some of the other logical rules:
inl : $σ → σ ∨ τ$
where $σ∨τ := ∀α.(σ→α)→(τ →α)→α$. I suppose one could use Definition 32 (p. 38) to derive $∀α.σ$ from $σ$ but that's about it (Definition 30 might be useful, too). No solutions are available and I'm not sure how to derive $α$ from $σ$ (should I just assume it?) or $σ→α$ from $σ$ or $∀α.(σ→α)→(τ →α)→α$ from $(σ→α)→(τ→α)→α$ or whatever other option there might be. Any ideas? Hints?