update in static_2

[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 967c4c0e64abbc5eda2b564e9954fe0c9e0b0faa..1b50d4cd5b5e5bed59c36120c67dd8453ea0851f 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,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 →
-                     â\88\80b,f. â¬\87*[b,f] L1 â\89\98 K1 â\86\92 â¬\87*[b,f] L2 ≘ K2 →
-                     â\88\80U. â¬\86*[f] T ≘ U → L1 ≛[U] L2.
+                     â\88\80b,f. â\87©*[b,f] L1 â\89\98 K1 â\86\92 â\87©*[b,f] L2 ≘ K2 →
+                     â\88\80U. â\87§*[f] T ≘ U → L1 ≛[U] L2.
 /3 width=9 by rex_lifts_bi, tdeq_lifts_sn/ qed-.
 
 (* Forward lemmas with length for local environments ************************)