X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Flsubsv_ldrop.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Flsubsv_ldrop.ma;h=31d47c8c586bb4e36c16d4917826b9d3667f731d;hb=29973426e0227ee48368d1c24dc0c17bf2baef77;hp=f8caa3aee1a0bca3568538cb2a5853531d296c18;hpb=f95f6cb21b86f3dad114b21f687aa5df36088064;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma
index f8caa3aee..31d47c8c5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma
@@ -19,9 +19,9 @@ include "basic_2/dynamic/lsubsv.ma".
 (* Properties concerning basic local environment slicing ********************)
 
 (* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
+lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 →
                             ∀K1,e. ⇩[0, e] L1 ≡ K1 →
-                            ∃∃K2. h ⊢ K1 ¡⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
+                            ∃∃K2. h ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L2 ≡ K2.
 #h #g #L1 #L2 #H elim H -L1 -L2
 [ /2 width=3/
 | #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
@@ -42,9 +42,9 @@ lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
 qed-.
 
 (* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
+lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 →
                              ∀K2,e. ⇩[0, e] L2 ≡ K2 →
-                             ∃∃K1. h ⊢ K1 ¡⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
+                             ∃∃K1. h ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L1 ≡ K1.
 #h #g #L1 #L2 #H elim H -L1 -L2
 [ /2 width=3/
 | #I #L1 #L2 #V #_ #IHL12 #K2 #e #H