In S.C.Kleene, Introduction to Metamathematics (1952) , I've found difficulty with the proof of 148 (preliminary to least number principle) :
$\vdash \exists y[y < x \land A(y) \land \forall z( z < y \rightarrow \lnot A(z))] \lor \forall y[ y < x \rightarrow \lnot A(y)]$
Revised following Max's comments.
The proof is :
Proof by induction on x (formula 148 is $P(x) \lor Q(x)$).
Basis: $\vdash \lnot y < 0$ ; using $\vdash \lnot A \rightarrow (A \rightarrow B )$ derive $P(0) \lor Q(0)$ by $\rightarrow$-elim, $\forall$-intro and $\lor$-intro.
Induction step: assume $P(x) \lor Q(x)$ and by cases :
[1] $P(x) \vdash P(x’)$, by $\land$-elim, 135a, 134a and $\land$-intro, and then $P(x’) \lor Q(x’)$, by $\lor$-intro.
[2] $Q(x)$ by cases with $A(x) \lor \lnot A(x)$ :
[2a] $Q(x), A(x) \vdash P(x')$ [Kleene's hint: using 135a]
We have that : $\vdash x < x′$ (by 135a), and $A(x) \vdash A(x)$, and $Q(x) \vdash \forall z (z < y \rightarrow \lnot A(z))$ (changing bound variable, by Lemma 15a).
Then $Q(x), A(x) \vdash \exists y[y < x \land A(y) \land \forall z( z < y \rightarrow \lnot A(z))]$ (by $\land$-intro and $\exists$-intro) i.e. $P(x') \vdash P(x’) \lor Q(x’)$, by $\lor$-intro.
[2b] $Q(x), \lnot A(x) \vdash Q(x')$ [Kleene's hint : using 138a]
We have that : $\vdash y < x′ \rightarrow y < x \lor y = x$, and $Q(x) \vdash y < x \rightarrow \lnot A(y)$, and $\lnot A(x) \vdash y = x \rightarrow \lnot A(y)$.
Assembling all together : $Q(x), \lnot A(x) \vdash \forall y (y < x' \lor \lnot A(y))$ (by $\forall$-intro) i.e. $Q(x') \vdash P(x’) \lor Q(x’)$, by $\lor$-intro.
