= Solution
Choose arbitrary fresh variables $y,x,z$ and assume $H=((x=y\lor y=z)\land P(y))$ under label $a$. The <conjunction elimination rule> gives $x=y\lor y=z$ and $P(y)$. Apply the <disjunction elimination rule> to the equality disjunction.
In the case $x=y$, the supplied symmetry rule gives $y=x$, and the <equality elimination rule> applied to $P(y)$ gives $P(x)$. <Disjunction introduction rule> gives $P(x)\lor P(z)$. In the case $y=z$, <equality elimination rule> applied directly to $P(y)$ gives $P(z)$; the other <disjunction introduction rule> gives the same conclusion $P(x)\lor P(z)$. Discharge the two equality case assumptions by <disjunction elimination rule>.
Discharge $a$ with the <implication introduction rule>. There are now no undischarged assumptions. Use the <universal quantifier introduction rule> successively for $z$, then $x$, then $y$, yielding
$$
\forall y\,\forall x\,\forall z\,\bigl(((x=y\lor y=z)\land P(y))\to(P(x)\lor P(z))\bigr).
$$
Freshness holds at every generalization because the sole temporary assumption has already been discharged; the arbitrary variables are not tied to any premise.
Back to article page
