X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Flveq_length.ma;h=b97d967fa12da0a03e6617f76b6a084d83e8ec79;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=7f77340e77d8cdad5f3691b73373630967733587;hpb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
index 7f77340e7..b97d967fa 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
@@ -79,14 +79,14 @@ lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
 /3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, plus_to_minus_2/ qed-.
 
 lemma lveq_fwd_abst_bind_length_le: ∀I1,I2,L1,L2,V1,n1,n2.
-                                    L1.ⓑ{I1}V1 ≋ⓧ*[n1,n2] L2.ⓘ{I2} → |L1| ≤ |L2|.
+                                    L1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2.ⓘ[I2] → |L1| ≤ |L2|.
 #I1 #I2 #L1 #L2 #V1 #n1 #n2 #HL
 lapply (lveq_fwd_pair_sn … HL) #H destruct
 elim (lveq_fwd_length … HL) -HL >length_bind >length_bind //
 qed-.
 
 lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2.
-                                    L1.ⓘ{I1} ≋ⓧ*[n1,n2] L2.ⓑ{I2}V2 → |L2| ≤ |L1|.
+                                    L1.ⓘ[I1] ≋ⓧ*[n1,n2] L2.ⓑ[I2]V2 → |L2| ≤ |L1|.
 /3 width=6 by lveq_fwd_abst_bind_length_le, lveq_sym/ qed-.
 
 (* Inversion lemmas with length for local environments **********************)
@@ -95,7 +95,7 @@ lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2.ⓧ → |L1|
                                ∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 0 = n1 & ↑m2 = n2.
 #L1 #L2 #n1 #n2 #H #HL12
 lapply (lveq_fwd_length_plus … H) normalize >plus_n_Sm #H0
-lapply (plus2_inv_le_sn … H0 HL12) -H0 -HL12 #H0
+lapply (plus2_le_sn_sn … H0 HL12) -H0 -HL12 #H0
 elim (le_inv_S1 … H0) -H0 #m2 #_ #H0 destruct
 elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/
 qed-.