-theorem cpr_Omega_21: ∀h,G,L,W. ⦃G, L⦄ ⊢ Omega2 W ➡[h] Omega1 W.
-#h #G #L #W1 elim (lifts_total W1 (𝐔❴1❵))
-/5 width=5 by lifts_flat, cpm_zeta, cpm_eps, cpm_appl, cpm_delta, Delta_lifts/
-qed.
+theorem cpr_Omega_23 (h) (G) (L) (s): ⦃G, L⦄ ⊢ Omega2 s ➡[h] Omega3 s.
+/5 width=3 by cpm_eps, cpm_appl, cpm_bind, cpm_delta, Delta_lifts/ qed.
+
+theorem cpr_Omega_31 (h) (G) (L) (s): ⦃G, L⦄ ⊢ Omega3 s ➡[h] Omega1 s.
+/4 width=3 by cpm_zeta, Delta_lifts, lifts_flat/ qed.
+
+(* Main inversion properties ************************************************)
+
+theorem cpr_inv_Omega1_sn (h) (G) (L) (s):
+ ∀X. ⦃G, L⦄ ⊢ Omega1 s ➡[h] X →
+ ∨∨ Omega1 s = X | Omega2 s = X.
+#h #G #L #s #X #H elim (cpm_inv_appl1 … H) -H *
+[ #W2 #T2 #HW2 #HT2 #H destruct
+ <(cpr_inv_Delta_sn … HW2) -W2
+ <(cpr_inv_Delta_sn … HT2) -T2
+ /3 width=1 by refl, or_introl/
+| #p #V2 #W1 #W2 #T1 #T2 #HV #HW #HT whd in ⊢ (??%?→?); #H1 #H2 destruct
+ <(cpr_inv_Delta_sn … HV) -V2
+ >(cpr_inv_sort1 … HW) -W2
+ <(cpr_inv_Delta1_body_sn … HT) -T2 //
+| #p #V2 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ whd in ⊢ (??%?→?); #H #_ destruct
+]
+qed-.
+
+theorem cpr_Omega_21_false (h) (G) (L) (s): ⦃G, L⦄ ⊢ Omega2 s ➡[h] Omega1 s → ⊥.
+#h #G #L #s #H elim (cpm_inv_bind1 … H) -H *
+[ #W #T #_ #_ whd in ⊢ (??%?→?); #H destruct
+| #X #H #_ #_ #_
+ elim (lifts_inv_flat2 … H) -H #X1 #X2 #H1 #_ #_
+ @(lifts_inv_lref2_uni_lt … H1) -H1 //
+]
+qed-.