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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
index 85419d1eaa3b9358a2e87815f9b5a998855a2853..3b55fca9920e66a6a8be3f1a163cae1097a237c0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
@@ -94,6 +94,6 @@ lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → (T1 = T2 → 
 ]
 qed.
 
-lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) →
+lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → (L1 = L2 → ⊥) →
                   h ⊢ ⦃L1, T⦄ >[g] ⦃L2, T⦄.
 /4 width=1/ qed.