-lemma cpr_ApplOmega_23 (h): ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega2 W s ➡[h] ApplOmega3 W s.
-#h #G #L #W1 #s elim (lifts_total W1 (𝐔❴1❵)) #W2 #HW12
-@(cpm_zeta … (ApplOmega3 W2 s)) /4 width=1 by ApplDelta_lifts, lifts_flat/
-@cpm_appl // @cpm_appl @(cpm_delta … (ApplDelta W1 s))
-/2 width=1 by ApplDelta_lifts, cpm_eps/
-qed.
+lemma cpr_ApplOmega_23 (h) (G) (L) (s0) (s): ⦃G,L⦄ ⊢ ApplOmega2 s0 s ➡[h] ApplOmega3 s0 s.
+/6 width=3 by cpm_eps, cpm_appl, cpm_bind, cpm_delta, ApplDelta_lifts/ qed.
+
+lemma cpr_ApplOmega_34 (h) (G) (L) (s0) (s): ⦃G,L⦄ ⊢ ApplOmega3 s0 s ➡[h] ApplOmega4 s0 s.
+/4 width=3 by cpm_zeta, ApplDelta_lifts, lifts_sort, lifts_flat/ qed.