\begin{proposition}\label{trivial}
    $x = x$.
\end{proposition}

\begin{proposition}\label{irrelevant}
    $z = z$.
\end{proposition}

\begin{proposition}\label{alsotrivial}
    $y = y$.
\end{proposition}
\begin{proof}
    \begin{align*}
        y
            &= y
                \\
            &= y
                \explanation{by \cref{trivial}}
    \end{align*}
\end{proof}

\begin{proposition}\label{trivial_biconditionals}
    $y = y$.
\end{proposition}
\begin{proof}
    \begin{align*}
        y = y
            &\iff \top
                \\
            &\iff y = y
                \explanation{by \cref{trivial}}
    \end{align*}
\end{proof}

\begin{proposition}\label{bounded_calc}
    For all $x \in A$ we have $x = x$.
\end{proposition}
\begin{proof}
    For all $x \in A$ we have
    \begin{align*}
        x
            &= x
    \end{align*}
\end{proof}

\begin{proposition}\label{bounded_calc_such_that}
    For all $x \in A$ such that $x = x$ we have $x = x$.
\end{proposition}
\begin{proof}
    For all $x \in A$ such that $x = x$, we have
    \begin{align*}
        x
            &= x
    \end{align*}
\end{proof}