-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 ]
+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/