diff --git a/docs/logic.tex b/docs/logic.tex
index 01d904d71ef8edf12da59d84654008e63779814d..a8e7552ad6476158a90506a0d0a044a03f86d610 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -417,7 +417,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 \begin{mathpar}
 \begin{array}{rMcMl}
 \ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff&  \ownGGhost{\melt \mtimes \meltB} \\
-\ownGGhost{\melt} &\provesIff& \mval(\melt) \\
+\ownGGhost{\melt} &\proves& \mval(\melt) \\
 \TRUE &\proves&  \ownGGhost{\munit}
 \end{array}
 \and