some restyling ...

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

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 c5b0e5f311fab2b781bf46a41f99b69d66ceb7d9..967c4c0e64abbc5eda2b564e9954fe0c9e0b0faa 100644 (file)
--- 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-.