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

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqx_length.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqx_length.ma
index d8750ca24..dafdc4f57 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/reqx_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/reqx_length.ma
@@ -39,7 +39,7 @@ lemma reqx_gref_length: ∀L1,L2. |L1| = |L2| → ∀l. L1 ≛[§l] L2.
 /2 width=1 by rex_gref_length/ qed.
 
 lemma reqx_unit_length: ∀L1,L2. |L1| = |L2| →
-                        ∀I. L1.ⓤ{I} ≛[#0] L2.ⓤ{I}.
+                        ∀I. L1.ⓤ[I] ≛[#0] L2.ⓤ[I].
 /2 width=1 by rex_unit_length/ qed.
 
 (* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *)