(* Basic inversion properties ***********************************************)
lemma cpr_inv_Delta1_body_sn (h) (G) (L) (s):
- â\88\80X. â\9dªG,L.â\93\9bâ\8b\86sâ\9d« â\8a¢ â\93\90#O.#O â\9e¡[h] X → ⓐ#O.#O = X.
+ â\88\80X. â\9d¨G,L.â\93\9bâ\8b\86sâ\9d© â\8a¢ â\93\90#O.#O â\9e¡[h,0] X → ⓐ#O.#O = X.
#h #G #L #s #X #H
lapply (cpm_inv_appl1 … H) -H * *
[ #W2 #T2 #HW2 #HT2 #H destruct
qed-.
lemma cpr_inv_Delta_sn (h) (G) (L) (s):
- â\88\80X. â\9dªG,Lâ\9d« â\8a¢ Delta s â\9e¡[h] X → Delta s = X.
+ â\88\80X. â\9d¨G,Lâ\9d© â\8a¢ Delta s â\9e¡[h,0] X → Delta s = X.
#h #G #L #s #X #H
elim (cpm_inv_abst1 … H) -H #X1 #X2 #H1 #H2 #H destruct
lapply (cpr_inv_sort1 … H1) -H1 #H destruct
(* Main properties **********************************************************)
-theorem cpr_Omega_12 (h) (G) (L) (s): â\9dªG,Lâ\9d« â\8a¢ Omega1 s â\9e¡[h] Omega2 s.
+theorem cpr_Omega_12 (h) (G) (L) (s): â\9d¨G,Lâ\9d© â\8a¢ Omega1 s â\9e¡[h,0] Omega2 s.
/2 width=1 by cpm_beta/ qed.
-theorem cpr_Omega_23 (h) (G) (L) (s): â\9dªG,Lâ\9d« â\8a¢ Omega2 s â\9e¡[h] Omega3 s.
+theorem cpr_Omega_23 (h) (G) (L) (s): â\9d¨G,Lâ\9d© â\8a¢ Omega2 s â\9e¡[h,0] 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): â\9dªG,Lâ\9d« â\8a¢ Omega3 s â\9e¡[h] Omega1 s.
+theorem cpr_Omega_31 (h) (G) (L) (s): â\9d¨G,Lâ\9d© â\8a¢ Omega3 s â\9e¡[h,0] 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):
- â\88\80X. â\9dªG,Lâ\9d« â\8a¢ Omega1 s â\9e¡[h] X →
+ â\88\80X. â\9d¨G,Lâ\9d© â\8a¢ Omega1 s â\9e¡[h,0] 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
]
qed-.
-theorem cpr_Omega_21_false (h) (G) (L) (s): â\9dªG,Lâ\9d« â\8a¢ Omega2 s â\9e¡[h] Omega1 s → ⊥.
+theorem cpr_Omega_21_false (h) (G) (L) (s): â\9d¨G,Lâ\9d© â\8a¢ Omega2 s â\9e¡[h,0] Omega1 s → ⊥.
#h #G #L #s #H elim (cpm_inv_bind1 … H) -H *
[ #W #T #_ #_ whd in ⊢ (??%?→?); #H destruct
| #X #H #_ #_ #_