/5 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
lemma cpr_ApplOmega_12: ∀G,L,W,k. ⦃G, L⦄ ⊢ ApplOmega1 W k ➡ ApplOmega2 W k.
/5 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
lemma cpr_ApplOmega_12: ∀G,L,W,k. ⦃G, L⦄ ⊢ ApplOmega1 W k ➡ ApplOmega2 W k.