lemma csx_ind: ∀h,o,G,L. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) →
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → R T2) →
R T1
) →
∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
(* Basic_1: was just: sn3_pr2_intro *)
lemma csx_intro: ∀h,o,G,L,T1.
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) →
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) →
⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄.
/4 width=1 by SN_intro/ qed.
-lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃⋆s⦄.
-#h #o #G #L #s elim (deg_total h o s)
-#d generalize in match s; -s elim d -d
-[ #s1 #Hs1 @csx_intro #X #H #HX elim HX -HX
- elim (cpx_inv_sort1 … H) -H #H destruct //
- /3 width=3 by tdeq_sort, deg_next/
-| #d #IH #s #Hsd lapply (deg_next_SO … Hsd) -Hsd
- #Hsd @csx_intro #X #H #HX
- elim (cpx_inv_sort1 … H) -H #H destruct /2 width=1 by/
- elim HX //
-]
-qed.
-
(* Basic forward lemmas *****************************************************)
fact csx_fwd_pair_sn_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ →