partial commit: just the components before "static" ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
index 6c5e0f6a5e7a6dd21b2d07bc144d3005d37c77c0..bb07981b0335dd4149270ed1ce8fe9cc882759f2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
@@ -21,9 +21,9 @@ include "basic_2/dynamic/lsubsv_ssta.ma".
 (* Properties on sn parallel reduction for local environments ***************)
 
 fact ssta_cpr_lpr_aux: ∀h,g,L0,T0.
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
                        ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_cpr_lpr h g L1 T1.
 #h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *]
 [ #k #_ #_ #_ #X2 #l #H2 #X3 #H3 #L2 #HL12 -IH3 -IH2 -IH1