update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / reqx_length.ma

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 d8750ca24157f907347e041d6782f4998d55a143..dafdc4f5716d1ff1a40bfbf506a17e4ba687db59 100644 (file)
--- 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 *)