blob: b0a0386522f4cc4527941da451aa13b24dee3c86 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
\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}
|
