\begin{proposition}\label{suffices_exact}
    Let $A$ be a set.
    $A=A$.
\end{proposition}
\begin{proof}
    It suffices to show that $A=A\land A=A$.
    Follows.
\end{proof}

\begin{proposition}\label{calculation_equality_exact}
    Let $A$ be a set.
    Suppose $A=\emptyset\land \emptyset=\{A\}$.
    Then $A=\{A\}$.
\end{proposition}
\begin{proof}
    \begin{align*}
        A
            &= \emptyset
                \explanation{by \cref{suffices_exact}}
            \\
            &= \{A\}
                \explanation{by assumption}
    \end{align*}
    Follows by assumption.
\end{proof}

\begin{proposition}\label{calculation_biconditional_exact}
    Let $A$ be a set.
    $(A=A)\iff ((A=A)\lor(A\neq A))$.
\end{proposition}
\begin{proof}
    \begin{align*}
        A=A
            &\iff \top
                \\
            &\iff (A=A)\lor(A\neq A)
                \explanation{by assumption}
    \end{align*}
    Follows by assumption.
\end{proof}

\begin{proposition}\label{calculation_quantified_exact}
    Let $A$ be a set.
    For all $x,y\in A$ such that $x=y$ we have $x=y$.
\end{proposition}
\begin{proof}
    For all $x,y\in A$ such that $x=y$, we have
    \begin{align*}
        x
            &= y
    \end{align*}
    Follows by assumption.
\end{proof}

\begin{proposition}\label{since_structural_exact}
    Let $A$ be a set.
    Suppose $A=A$.
    Then $A=A$.
\end{proposition}
\begin{proof}
    Since $A=A$, we have $A=A$ by assumption.
    Follows by assumption.
\end{proof}

\begin{proposition}\label{since_discharge_exact}
    Let $A,B$ be sets.
    Suppose $A=A$.
    Then $A=A$.
\end{proposition}
\begin{proof}
    Since $B=B$, we have $A=A$ by assumption.
    Follows by assumption.
\end{proof}

\begin{proposition}\label{suffices_omitted_exact}
    Let $A$ be a set.
    $A=A$.
\end{proposition}
\begin{proof}
    It suffices to show that $A=A$.
    Omitted.
\end{proof}