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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
index 30c90c43e003f1418cde79b01e33eb6f57a101b7..0c7231075f09e5917294e0e8f193d98977450693 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
@@ -69,7 +69,7 @@ lemma sstas_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 →
 #h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=4 by ypr_ssta, yprs_strap1/
 qed.
 
-lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
+lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
 /3 width=1/ qed.
 
 lemma ltpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ➡ L2 → L2 ⊢ T1 ➡* T2 →