# Understanding the definition of a "restriction of a resolution derivation"

I am reading the paper An Introduction to Lower Bounds on Resolution Proof Systems. In its subsection 2.3 the author gives an inductive definition of the restriction of a resolution refutation $\pi$. My preoccupation resides on the second line of the definition :

$C'_i=C'_{j_1} \vee C'_{j_2}$ if $C_{j_1} \vee y$ and $C_{j_2}\vee \bar{y}$ derive $C_i$ via the resolution rule for $j_1 < j_2 < i;$.

I wonder how this induction can be apply on $C'_{j_1}$ and $C'_{j_2}$ since $C_{j_1}$ and $C_{j_2}$ are not in $\pi$ but instead $C_{j_1}\vee y$ and $C_{j_2}\vee \bar{y}$.

Furthermore, in example 2.12 the author computes the restrictions $\pi[x_1=0]$ and $\pi[x_2=1]$ of the refutation $\pi$ as if they were just a restrictions of sets of clauses i.e. by using $\pi[x=a]=\{C[x=a]; C \in \pi\}$ instead of the inductive definition.

Is there anything that I'm missing?

For the first point, it seems that $C_{j_1} := D_{j_1} \lor y$ and $C_{j_2} := D_{j_2} \lor \bar{y}$ are meant to be the clauses in $\pi$, instead of $C_{j_1} \lor y$ and $C_{j_2} \lor \bar{y}$. This may help in understanding such a definition. Furthermore, it seems that the resolution of $C'_{j_1}$ and $C'_{j_2}$ upon $y$ is taken, rather than $C'_{j_1} \lor C'_{j_2}$ (they are equivalent). This view would explain, for example, the computation of $C_4[x=0]$: $C_1' = x_2 \lor \bar{x_3}$ and $C_2' = x_3$ are resolved upon $x_3$ to obtain $C_4' = x_2$.