\begin{proposition}\label{phase5_fixed_set_induction} For all sets $x$ we have $x=x$. \end{proposition} \begin{proof} Fix $x$. Show $x=x$. \begin{subproof}[Proof by \in-induction on $x$] Follows. \end{subproof} Follows by assumption. \end{proof}