X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_cpxs.ma;h=ae3d9a8892e37ac4d46ce87b0732aaf7c25f9c32;hb=6555775aa5268dec0d9ae4579412b659cacdc964;hp=1b4c9cb520b17d0c0fdfc9485926dbdef1c4f93b;hpb=69592aa1d0c0d122fb09f11cc53bf4c5a1532fdd;p=helm.git

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 1b4c9cb52..ae3d9a889 100644
--- 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-.