so $L \in \py$ so $L \haspatch \p$. We will use the coherence and
patch inclusion of $C$ as just proved.
Firstly we prove $C \haspatch \p$: If $R \in \py$, this is true by
so $L \in \py$ so $L \haspatch \p$. We will use the coherence and
patch inclusion of $C$ as just proved.
Firstly we prove $C \haspatch \p$: If $R \in \py$, this is true by