diff --git a/docs/algebra.tex b/docs/algebra.tex index e9b3208e454bd5e1316827bbea1a5be8f0b3c999..e5638382353fac9b6de1b1f0975752bd47094dca 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -168,7 +168,6 @@ This operation is needed to prove that $\later$ commutes with separating conjunc \item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$ \item $\munit$ is a left-identity of the operation: \\ $\All \melt \in M. \munit \mtimes \melt = \melt$ - \item $\munit$ is a discrete COFE element \item $\munit$ is its own core: \\ $\mcore\munit = \munit$ \end{enumerate} \end{defn}