X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fst_computation.ma;h=ebcc572a40b403cd4f8ee3021279d7d87e0db210;hb=bde429ac54e48de74b3d8b1df72dfcb86aa9bae5;hp=a7ccb05fd58a58de843e2ececc5ad65f53a9ca7e;hpb=4bb6799d029b7b377f7aa28b0e90f0a69c149a9c;p=helm.git

diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma
index a7ccb05fd..ebcc572a4 100644
--- a/matita/matita/contribs/lambda/st_computation.ma
+++ b/matita/matita/contribs/lambda/st_computation.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "labelled_sequential_computation.ma".
+include "labeled_sequential_computation.ma".
 include "pointer_list_standard.ma".
 
 (* KASHIMA'S "ST" COMPUTATION ***********************************************)
@@ -151,7 +151,7 @@ lemma st_inv_lsreds_is_standard: ∀M,N. M ⓢ⤇* N →
 [ #s #M #i #Hs #HM
   lapply (is_whd_is_standard … Hs) -Hs /2 width=3/
 | #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr
-  lapply (lsreds_trans … HM (sn:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
+  lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
   @(ex2_intro … HM) -M -A2 /3 width=1/
 | #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
   lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM