-lemma cpr_ApplOmega_23: ∀G,L,W,k. ⦃G, L⦄ ⊢ ApplOmega2 W k ➡ ApplOmega3 W k.
-#G #L #W1 #k elim (lift_total W1 0 1) #W2 #HW12
-@(cpr_zeta … (ApplOmega3 W2 k)) /4 width=1 by ApplDelta_lift, lift_flat/
-@cpr_flat // @cpr_flat @(cpr_delta … (ApplDelta W1 k) ? 0)
+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)