X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Flveq_lveq.ma;h=f3b2d18cd8a98b255331ad25e327493a900f7a7b;hp=c0c8cf1abfba2c9b32f208839e8351ccb7bcb663;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma
index c0c8cf1ab..f3b2d18cd 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma
@@ -19,7 +19,7 @@ include "static_2/syntax/lveq_length.ma".
 (* Main inversion lemmas ****************************************************)
 
 theorem lveq_inv_bind: ∀K1,K2. K1 ≋ⓧ*[0,0] K2 →
-                       ∀I1,I2,m1,m2. K1.ⓘ{I1} ≋ⓧ*[m1,m2] K2.ⓘ{I2} →
+                       ∀I1,I2,m1,m2. K1.ⓘ[I1] ≋ⓧ*[m1,m2] K2.ⓘ[I2] →
                        ∧∧ 0 = m1 & 0 = m2.
 #K1 #K2 #HK #I1 #I2 #m1 #m2 #H
 lapply (lveq_fwd_length_eq … HK) -HK #HK