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.