diff --git a/draft/draft.tex b/draft/draft.tex
index 78069c9..f821024 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -2171,7 +2171,7 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the
 \begin{cor}
 	Considering~\autoref{lem:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well.
 \end{cor}
-
+Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor.
 \subsection{Maybe Functor}
 We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_X\cup\{(\bot,x)\mid x\in X\}$.
 \begin{lemma}\label{lem:maybe-func-set}