Proving $\alpha \implies \alpha$ is derivable I'm going through Goldblatt's "Topoi", and one of the exercises there depends upon proving that a certain axiom system entails $\alpha \implies \alpha$ for any proposition $\alpha$.
The axiom system in question is as follows (paragraph 6.3):

*

*$ \alpha \implies (\alpha \land \alpha) $

*$ (\alpha \land \beta) \implies (\beta \land \alpha) $

*$ (\alpha \implies \beta) \implies ((\alpha \land \gamma) \implies (\beta \land \gamma)) $

*$ ((\alpha \implies \beta) \land (\beta \implies \gamma)) \implies (\alpha \implies \gamma) $

*$ \beta \implies (\alpha \implies \beta) $

*$ (\alpha \land (\alpha \implies \beta)) \implies \beta $

*$ \alpha \implies (\alpha \lor \beta) $

*$ (\alpha \lor \beta) \implies (\beta \lor \alpha) $

*$ ((\alpha \implies \gamma) \land (\beta \implies \gamma)) \implies ((\alpha \lor \beta) \implies \gamma) $

*$ \lnot \alpha \implies (\alpha \implies \beta) $

*$ ((\alpha \implies \beta) \land (\alpha \implies \lnot \beta)) \implies \lnot \alpha $

*$ \alpha \lor \lnot \alpha $
The sole inference rule is the usual modus ponens.
So, it feels like the axiom (9) together with (12) can be used as the last step of the derivation (instantiating $\alpha$ to $\alpha$, $\beta$ to $\lnot \alpha$ and $\gamma$ to $\alpha \implies \alpha$). Then, the left-hand side of the $\land$ in (9) can be derived using (5), and the right-hand side can be derived using (10). But how do I combine those under a $\land$? Looks like I don't have a usual $\land$-introduction rule — axiomatic systems I've seen before typically have something of the form $\alpha \implies (\beta \implies (\alpha \land \beta))$.
Also, resorting to the (non-constructive) axiom of excluded middle for this obviously constructive statement feels just wrong.
So what's the right way to prove $\alpha \implies \alpha$ in this system?
 A: Well, before I lose it, here's what Prover9 gave me after translation into a prefix notation.  C(x, y) gets used instead of (x⟹y).  K(x,y) instead of (x∧y).  N(x) instead of $\lnot$x.  And A(x,y) instead of (x$\lor$y).:
% -------- Comments from original proof --------
% Proof 1 at 1.19 (+ 0.56) seconds.
% Length of proof is 16.
% Level of proof is 6.
% Maximum clause weight is 14.
% Given clauses 812.
1 P(C(x,x)) # label(non_clause) # label(goal).  [goal].
2 -P(C(x,y)) | -P(x) | P(y).  [assumption].
3 P(C(x,K(x,x))).  [assumption].
5 P(C(C(x,y),C(K(x,z),K(y,z)))).  [assumption].
7 P(C(x,C(y,x))).  [assumption].
11 P(C(K(C(x,y),C(z,y)),C(A(x,z),y))).  [assumption].
12 P(C(N(x),C(x,y))).  [assumption].
14 P(A(x,N(x))).  [assumption].
15 -P(C(c1,c1)).  [deny(1)].
24 P(C(x,C(y,C(z,y)))).  [hyper(2,a,7,a,b,7,a)].
55 P(K(C(N(x),C(x,y)),C(N(x),C(x,y)))).  [hyper(2,a,3,a,b,12,a)].
99 P(C(K(x,y),K(C(z,C(u,z)),y))).  [hyper(2,a,5,a,b,24,a)].
1001 P(K(C(x,C(y,x)),C(N(z),C(z,u)))).  [hyper(2,a,99,a,b,55,a)].
11705 P(C(A(x,N(y)),C(y,x))).  [hyper(2,a,11,a,b,1001,a)].
11723 P(C(x,x)).  [hyper(2,a,11705,a,b,14,a)].
11724 $F.  [resolve(11723,a,15,a)].
A: Pasting the image since the line breaking makes the text unreadable...

