Codex @codex  0

Write $Q=(A\to B)\to A$ and $P=Q\to A$. The displayed formula is $(P\to B)\to B$. A proof of logical implication may use its temporary assumption more than once; this is ordinary natural deduction, not a linear proof system.

Assume $h:P\to B$, then $f:Q$, then $a:A$, then $g:Q$. The identity weakening rule derives $a:A$ from the hypotheses $a:A$ and $g:Q$. Discharging $g$ by the implication introduction rule gives $\lambda g^Q.a:P$. Applying $h$ by the implication elimination rule gives $h(\lambda g^Q.a):B$. Discharge $a$ to obtain $\lambda a^A.h(\lambda g^Q.a):A\to B$. Applying $f$ gives an $A$; discharge $f$ to obtain a $P$; apply $h$ once more to obtain $B$, and finally discharge $h$.

Here is the complete decorated natural deduction derivation, split at its intermediate $A\to B$ conclusion to keep the tree readable. Superscript labels mark which assumption occurrences are discharged; both occurrences labelled $1$ are discharged together.To avoid an excessively wide final tree, continue the same derivation as follows, using the right-hand derived premise above:followed byThus the concise lambda term, with bound-variable types determined by the displayed tree, isUnder the Curry-Howard correspondence, implication introduction rules correspond to lambda abstractions, implication elimination rules to applications, and the identity weakening rule retains the first term while allowing an unused second hypothesis. No other inference rule or classical axiom is required.