minor

draft/draft.tex

@@ -1915,7 +1915,7 @@ We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
 %\begin{rem}
 %	Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation.
 %\end{rem}
-Since $\subseteq$ is a liftable order, we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. An abstract version of the following lemma is given by Dubut.
+Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. An abstract version of the following lemma is given by Dubut.
 \begin{lemma}\label{lem:alph-prod}
 	Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, where $\powf p_1\comp\sigma'=\alpha\comp p_1$. 
 \end{lemma}