fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\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⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\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⦄ ⊢ T ⁝ A → R T.
/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\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⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
(* Basic_2A1: was: aaa_ind_csx_alt *)
lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\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⦄ ⊢ T ⁝ A → R T.
/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-.