From 9484eea8e08b6684b49046dbbc50dd8173647245 Mon Sep 17 00:00:00 2001
From: Mike Shulman <viritrilbia@gmail.com>
Date: Tue, 8 Sep 2015 09:44:33 -0700
Subject: [PATCH] refer to Corollary 3.2.7 in Lemma 7.2.4

---
 hlevels.tex | 1 +
 1 file changed, 1 insertion(+)

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$,