X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fltpss_sn_tpss.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fltpss_sn_tpss.ma;h=007613cf9562d1f69c5e4768b5f7365f0cde819d;hb=bd7183da46c7cb0f389cda40955b270c03b57a4b;hp=d23c1a255bac16a8d0cc7989733f6c52dc857d59;hpb=cdfd45ca5a2b52601b7bde732a7811de55a52fed;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma
index d23c1a255..007613cf9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma
@@ -52,7 +52,7 @@ lemma ltpss_sn_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
 | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
   elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
   elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 #T #HT2 #H
-  lapply (tpss_lsubs_trans … H (L0.ⓑ{I}V) ?) -H /2 width=1/ /3 width=5/
+  lapply (tpss_lsubr_trans … H (L0.ⓑ{I}V) ?) -H /2 width=1/ /3 width=5/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
   elim (IHVW2 … HL01) -IHVW2
   elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
@@ -93,7 +93,7 @@ lemma ltpss_sn_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
 | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
   elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
   elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 #T #HT2 #H
-  lapply (tpss_lsubs_trans … H (L1.ⓑ{I}W2) ?) -H /2 width=1/ /3 width=5/
+  lapply (tpss_lsubr_trans … H (L1.ⓑ{I}W2) ?) -H /2 width=1/ /3 width=5/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
   elim (IHVW2 … HL10) -IHVW2
   elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/