X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Frdeq_length.ma;h=967c4c0e64abbc5eda2b564e9954fe0c9e0b0faa;hp=c5b0e5f311fab2b781bf46a41f99b69d66ceb7d9;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rdeq_length.ma b/matita/matita/contribs/lambdadelta/static_2/static/rdeq_length.ma
index c5b0e5f31..967c4c0e6 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/rdeq_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rdeq_length.ma
@@ -44,7 +44,7 @@ lemma rdeq_unit_length: ∀L1,L2. |L1| = |L2| →
 
 (* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *)
 lemma rdeq_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ≛[T] K2 →
-                     ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 →
+                     ∀b,f. ⬇*[b,f] L1 ≘ K1 → ⬇*[b,f] L2 ≘ K2 →
                      ∀U. ⬆*[f] T ≘ U → L1 ≛[U] L2.
 /3 width=9 by rex_lifts_bi, tdeq_lifts_sn/ qed-.