- advances towards strong normalization

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx_cpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
index 1b4c9cb520b17d0c0fdfc9485926dbdef1c4f93b..ae3d9a8892e37ac4d46ce87b0732aaf7c25f9c32 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
@@ -58,11 +58,12 @@ elim (tdeq_dec h o T1 T0) #H
 ]
 qed-.
 
-lemma csx_ind_alt: ∀h,o,G,L. ∀R:predicate term.
-                   (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
-                         (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
-                   ) →
-                   ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
+(* Basic_2A1: was: csx_ind_alt *)
+lemma csx_ind_cpxs: ∀h,o,G,L. ∀R:predicate term.
+                    (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
+                          (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+                    ) →
+                    ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
 #h #o #G #L #R #IH #T #HT
 @(csx_ind_cpxs_tdeq … IH … HT) -IH -HT // (**) (* full auto fails *)
 qed-.