diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf
index 9a0f62f..99ad126 100644
Binary files a/semester4/fmfp/formal-methods-functional-programming-summary.pdf and b/semester4/fmfp/formal-methods-functional-programming-summary.pdf differ
diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex
index 17dc900..03b0e4e 100644
--- a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex
+++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex
@@ -36,7 +36,7 @@ In IMP however, this kind of action leads to equivalence:
 \]
 So what we have to prove is this:
 \[
-    \forall b, s, \sigma, \sigma'.(\vdash \langle \texttt{while b do s end}, \sigma \rangle \; \simeq \;
+    \forall b, s, \sigma, \sigma'.(\vdash \langle \texttt{while b do s end}, \sigma \rangle \; \Leftrightarrow \;
     \vdash \langle \texttt{if b then s; while b do s end end}, \sigma \rangle \rightarrow \sigma')
 \]