X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Flsubsv_ssta.ma;h=b85b4a8fa6a003ad0575f12b2671bc2d4c232634;hb=8ff4315142253a1a0478b67c07dddf70c36f50cd;hp=94db2292b6336b85310675172967670aa364f2d3;hpb=7abd5e0412171f7d07e085d334198c034895c2c3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
index 94db2292b..b85b4a8fa 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
@@ -12,15 +12,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/equivalence/lsubse_ssta.ma".
+include "basic_2/equivalence/lsubss_ssta.ma".
 include "basic_2/dynamic/lsubsv.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
 
 (* Properties on stratified static type assignment **************************)
 
-lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g,l] U2 →
+lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ →
                          ∀L1. h ⊢ L1 ⊩:⊑[g] L2 →
-                         ∃∃U1. ⦃h, L1⦄ ⊢ T •[g,l] U1 & L1 ⊢ U1 ⬌* U2.
-/3 width=3 by lsubsv_fwd_lsubse, lsubse_ssta_trans/
+                         ∃∃U1. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2.
+/3 width=3 by lsubsv_fwd_lsubss, lsubss_ssta_trans/
 qed-.