$\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor.

This fixed-point exists and is unique\footnote{We have not proven uniqueness in Coq.} by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.

We do not need to consider how the object is constructed.

We only need the isomorphism, given by

Here, $\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor, which exists by \thmref{thm:america_rutten}.

We do not need to consider how the object $\iPreProp$ is constructed, we only need the isomorphism, given by: