typo

martinescardo · Sep 3, 2023 · 7a82bce · 7a82bce
1 parent 614a7b7
commit 7a82bce
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/source/Fin/Omega.lagda b/source/Fin/Omega.lagda
@@ -197,4 +197,4 @@ Fin-to-Ω-embedding-is-equiv-iff-2-and-EM {𝓤} fe pe (succ (succ (succ k)))
 
 \end{code}
 
-TODO. Refactor the above prove in smaller meaningful components.
+TODO. Refactor the above proof in smaller meaningful components.