X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fypr.ma;h=c08c984f218ba68c7f1fd58faa3f6841bbfe61c8;hb=fdb2c62b58006b82c015ba70b494d50c7860e28f;hp=2c8c96d27a737e8975cb4927a2dac00ad701cac7;hpb=4aa431513ffa0ce0accf81e6e9ea4b9314d468e3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma
index 2c8c96d27..c08c984f2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma
@@ -23,7 +23,7 @@ inductive ypr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
 | ypr_fsup  : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ypr h g G1 L1 T1 G2 L2 T2
 | ypr_lpr   : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → ypr h g G1 L1 T1 G1 L2 T1
 | ypr_cpr   : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → ypr h g G1 L1 T1 G1 L1 T2
-| ypr_ssta  : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 •[h, g] ⦃l+1, T2⦄ → ypr h g G1 L1 T1 G1 L1 T2
+| ypr_ssta  : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G1, L1⦄ ⊢ T1 •[h, g] T2 → ypr h g G1 L1 T1 G1 L1 T2
 | ypr_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → ypr h g G1 L1 T1 G1 L2 T1
 .