diff --git a/hlevels.tex b/hlevels.tex
index f9791c940..fbfc6ccbd 100644
--- a/hlevels.tex
+++ b/hlevels.tex
@@ -331,6 +331,7 @@ \section{Uniqueness of identity proofs and Hedberg's theorem}
 \end{lem}
 
 \begin{proof}
+This was essentially already proven in \cref{thm:not-lem}, but we repeat the argument.
 Suppose $x:A+\neg A$. We have two cases to consider.
 If $x$ is $\inl(a)$ for some $a:A$, then we have the constant function $\neg\neg A
 \to A$ which maps everything to $a$. If $x$ is $\inr(t)$ for some $t:\neg A$,