-lemma cpr_ApplOmega_23: ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega2 W s ➡ ApplOmega3 W s.
-#G #L #W1 #s elim (lift_total W1 0 1) #W2 #HW12
-@(cpr_zeta … (ApplOmega3 W2 s)) /4 width=1 by ApplDelta_lift, lift_flat/
-@cpr_flat // @cpr_flat @(cpr_delta … (ApplDelta W1 s) ? 0)
-[3,5,8,10: /2 width=2 by ApplDelta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ]
-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.