lsubs renamed as lsubr

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / ltpss_sn_ltpss_sn.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
index dfcd35c73711860d3980013b8a28f4bc7c56674f..67c287e2bac0488a0fa5d3932918bbcdf06810f8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
@@ -32,10 +32,10 @@ lemma ltpss_sn_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
   lapply (tpss_trans_eq … HV01 HV12) -V1 /2 width=6/
 | * [ #a ] #I #V2 #T2 #Hn #X #d #e #H #L0 #HL0 destruct
   [ elim (tpss_inv_bind1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
-    lapply (tpss_lsubs_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
+    lapply (tpss_lsubr_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
     lapply (IH … HVW2 … HL0) -HVW2 [ /2 width=2/ ] #HVW2
     lapply (IH … HTU2 (L0. ⓑ{I} V2) ?) -IH -HTU2 // /2 width=2/ -HL0 #HTU2
-    lapply (tpss_lsubs_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
+    lapply (tpss_lsubr_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
   | elim (tpss_inv_flat1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
     lapply (IH … HVW2 … HL0) -HVW2 //
     lapply (IH … HTU2 … HL0) -IH -HTU2 // -HL0 /2 width=1/