add TODO

martinescardo · Sep 3, 2023 · 614a7b7 · 614a7b7
1 parent dc187ed
commit 614a7b7
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/source/Fin/Omega.lagda b/source/Fin/Omega.lagda
@@ -196,3 +196,5 @@ Fin-to-Ω-embedding-is-equiv-iff-2-and-EM {𝓤} fe pe (succ (succ (succ k)))
   I = finite-subsets-of-Ω-have-at-most-2-elements fe pe (succ (succ (succ k))) 𝕖
 
 \end{code}
+
+TODO. Refactor the above prove in smaller meaningful components.