qed-.
lemma cpr_inv_Delta_sn (h) (G) (L) (s):
- ∀X. ⦃G, L⦄ ⊢ Delta s ➡[h] X → Delta s = X.
+ ∀X. ⦃G,L⦄ ⊢ Delta s ➡[h] 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): ⦃G, L⦄ ⊢ Omega1 s ➡[h] Omega2 s.
+theorem cpr_Omega_12 (h) (G) (L) (s): ⦃G,L⦄ ⊢ Omega1 s ➡[h] Omega2 s.
/2 width=1 by cpm_beta/ qed.
-theorem cpr_Omega_23 (h) (G) (L) (s): ⦃G, L⦄ ⊢ Omega2 s ➡[h] Omega3 s.
+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.
+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 →
+ ∀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
]
qed-.
-theorem cpr_Omega_21_false (h) (G) (L) (s): ⦃G, L⦄ ⊢ Omega2 s ➡[h] Omega1 s → ⊥.
+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 #_ #_ #_