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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
index a1e54168ddb76f3c60717586e966738a3d13e61f..203cf3ebdfb3702ce36ba46e82e2ef2e04ea8086 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
@@ -20,7 +20,7 @@ inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝
 | ysc_fw    : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ysc h g L1 T1 L2 T2
 | ysc_cpr   : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2
 | ysc_ssta  : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ysc h g L1 T1 L1 T2
-| ysc_lsubsv: ∀L2. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1
+| ysc_lsubsv: ∀L2. h ⊢ L2 ¡⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1
 .
 
 interpretation