Define inl : $σ → σ ∨ τ$

Question

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: 1. Define 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?

Answer 1

It seems to me that the requested derivation is :

1) $\sigma$ --- assumed [1]

2) $\sigma \to \alpha$ --- assumed [2]

3) $\alpha$ --- from 1) and 2) by $\to$-E

4) $(\tau \to \alpha) \to \alpha$ --- from 3) by $\to$-I

5) $(\sigma \to \alpha) \to (\tau \to \alpha) \to \alpha$ --- from 2) and 4) by $\to$-I, discharging [2]

6) $\forall \alpha [(\sigma \to \alpha) \to (\tau \to \alpha) \to \alpha]$ --- from 5) by $\forall$-I : $\alpha \notin FV(\sigma)$

7) $\sigma \lor \tau$ --- definition of $\lor$

$\sigma \to \sigma \lor \tau$ --- from 1) and 7) by $\to$-I, discharging [1].