$z_{2k}\in Z_{2k}$, $k=1,\ldots,n-1$, with (setting $z_0=x$ and $z_{2n}=y$) $$f_{2k}(z_{2k})=f_{2k-1}(z_{2k-2}),\quad k=1,\ldots, n
    ,$$ then $x\sim y$.

We now recall the notion of a proper functor, introduced by Milius [@milius:2017] which is central to this paper. It is very helpful for establishing completeness of regular expressions calculi, cf. [@milius:2017 Corollary 3.17].

\[Proper\] Let $T\colon{{\text{\tt{Set}}}}\to{{\text{\tt{Set}}}}$ be a finitary monad with unit $\eta$ and multiplication $\mu$. A ${{\text{\tt{Set}}}^{T}}$-endofunctor $F$ is *proper*, if the following statement holds.

For each pair $(TB_1,c_1)$ and $(TB_2,c_2)$ of $F$-coalgebras with $B_1$ and $B_2$ finite sets, and each two elements $b_1\in B_1$ and $b_2\in B_2$ with $\eta_{B_1}(b_1)\sim\eta_{B_2}(b_2)$, there exists a zig-zag in ${{\sf Coalg}({F})}$ which relates $\eta_{B_1}(b_1)$ with $\eta_{B_2}(b_2)$, and whose nodes $(Z_j,e_j)$ all have free and finitely generated carrier.

This notion generalizes the notion of a proper semiring introduced by Esik and Maletti in [@esik.maletti:2010 Definition 3.2], cf. [@milius:2017 Remark 3.10].

\[fg\] In the definition of properness the condition that intermediate nodes have free *and* finitely generated carrier is necessary for nodes with incoming arrows (the nodes $Z_{2k-1}$ in ). For the intermediate nodes with outgoing arrows ($Z_{2k}$ in ), it is enough to require that their carrier is finitely generated. This follows since every $F$-coalgebra with finitely generated 