Merge pull request #865 from mikeshulman/lem-dne

refer to Corollary 3.2.7 in Lemma 7.2.4

Author: andrejbauer

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