notational change for snv and lsubsv: inverted "!" used for now

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / lsubsv_ssta.ma

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 b85b4a8fa6a003ad0575f12b2671bc2d4c232634..594c72662507e83af8f5efa25158f4d495ef1090 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
@@ -20,7 +20,7 @@ include "basic_2/dynamic/lsubsv.ma".
 (* Properties on stratified static type assignment **************************)
 
 lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ →
-                         ∀L1. h ⊢ L1 ⊩:⊑[g] L2 →
+                         ∀L1. h ⊢ L1 ¡⊑[g] L2 →
                          ∃∃U1. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2.
 /3 width=3 by lsubsv_fwd_lsubss, lsubss_ssta_trans/
 qed-.