update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / lveq_lveq.ma

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 c0c8cf1abfba2c9b32f208839e8351ccb7bcb663..f3b2d18cd8a98b255331ad25e327493a900f7a7b 100644 (file)
--- 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