X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Frdeq_length.ma;h=1b50d4cd5b5e5bed59c36120c67dd8453ea0851f;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=967c4c0e64abbc5eda2b564e9954fe0c9e0b0faa;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git

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 967c4c0e6..1b50d4cd5 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/rdeq_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rdeq_length.ma
@@ -44,8 +44,8 @@ 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 →
-                     ∀U. ⬆*[f] T ≘ U → L1 ≛[U] L2.
+                     ∀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-.
 
 (* Forward lemmas with length for local environments ************************)