-lemma cpr_ApplOmega_12 (h): ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡[h] ApplOmega2 W s.
-/2 width=1 by cpm_beta/ qed.
+lemma cpr_ApplOmega_12 (G) (L) (s0) (s):
+ ❪G,L❫ ⊢ ApplOmega1 s0 s ⬈ ApplOmega2 s0 s.
+/2 width=1 by cpx_beta/ qed.
+
+lemma cpr_ApplOmega_23 (G) (L) (s0) (s):
+ ❪G,L❫ ⊢ ApplOmega2 s0 s ⬈ ApplOmega3 s0 s.
+/6 width=3 by cpx_eps, cpx_flat, cpx_bind, cpx_delta, ApplDelta_lifts/ qed.