X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffsb_csx.ma;h=e3ad463a62b98704bfd70ee1e04a6ea1cfa3006c;hp=628b3b9df83b12affcd93c27593350c99a0d47ea;hb=bc27cc1925469ddcd2bc3cd4036a6ea8067c5da1;hpb=2b7797235d69608e4221b287480949961aaa3948

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
index 628b3b9df..e3ad463a6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
@@ -25,7 +25,7 @@ include "basic_2/rt_computation/fsb_fpbg.ma".
 
 lemma fsb_inv_csx:
       ∀G,L,T. ≥𝐒 ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒 T.
-#G #L #T #H @(fsb_ind_alt … H) -G -L -T
+#G #L #T #H @(fsb_ind … H) -G -L -T
 /5 width=1 by csx_intro, cpx_fpbc/
 qed-.
 
@@ -76,7 +76,7 @@ lemma csx_ind_fpbc (Q:relation3 …):
         Q G1 L1 T1
       ) →
       ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → Q G L T.
-/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
+/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind/ qed-.
 
 lemma csx_ind_fpbg (Q:relation3 …):
       (∀G1,L1,T1.