Solution (source code)

= Solution

Choose an auxiliary <propositional formula> $\beta$. The two instances of L1 are
$$
\alpha\to(\beta\to\alpha),\qquad
\alpha\to(\neg\beta\to\alpha).
$$
The instance of L2 with $\gamma=\alpha$ is
$$
(\alpha\to(\beta\to\alpha))\to
((\alpha\to(\neg\beta\to\alpha))\to(\alpha\to\alpha)).
$$
Apply <modus ponens rule> first with the first L1 instance and then with the second. This is an assumption-free <logical derivation>, so
$$
\boxed{\vdash\alpha\to\alpha.}
$$
In particular no semantic completeness theorem or <deduction theorem for propositional logic> has been assumed to obtain this identity theorem.