Cantor's Theorem

[knaeve]

https://github.com/OpenLogicProject/OpenLogic/blob/ad378487f3506a16aa8660ece130190898cf2578/content/sets-functions-relations/size-of-sets/reduction-alt.tex#L48-L50

On line 49, there's a minor typo.

\begin{proof}[Proof of {\olref[nen-alt]{thm:nonenum-pownat}} by reduction] 
 For reduction, suppose that $\Pow{\Nat}$ is !!{enumerable}, and thus that 
 there is an enumeration of it, $N_{1}$, $N_{2}$, $N_{3}$, \dots

[rzach]

Thanks!