update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / rpx_length.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_length.ma
index 58034f1571ebcdde9225940c22cc5bf477252e77..565a2498de2e8d0c675863ce918186dd9fca19fb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_length.ma
@@ -20,14 +20,14 @@ include "basic_2/rt_transition/rpx.ma".
 (* Forward lemmas with length for local environments ************************)
 
 lemma rpx_fwd_length (G):
-      â\88\80L1,L2,T. â\9dªG,L1â\9d« ⊢ ⬈[T] L2 → |L1| = |L2|.
+      â\88\80L1,L2,T. â\9d¨G,L1â\9d© ⊢ ⬈[T] L2 → |L1| = |L2|.
 /2 width=3 by rex_fwd_length/ qed-.
 
 (* Inversion lemmas with length for local environments **********************)
 
 lemma rpx_inv_zero_length (G):
-      â\88\80Y1,Y2. â\9dªG,Y1â\9d« ⊢ ⬈[#0] Y2 →
+      â\88\80Y1,Y2. â\9d¨G,Y1â\9d© ⊢ ⬈[#0] Y2 →
       ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
-       | â\88\83â\88\83I,L1,L2,V1,V2. â\9dªG,L1â\9d« â\8a¢ â¬\88[V1] L2 & â\9dªG,L1â\9d« ⊢ V1 ⬈ V2 & Y1 = L1.ⓑ[I]V1 & Y2 = L2.ⓑ[I]V2
+       | â\88\83â\88\83I,L1,L2,V1,V2. â\9d¨G,L1â\9d© â\8a¢ â¬\88[V1] L2 & â\9d¨G,L1â\9d© ⊢ V1 ⬈ V2 & Y1 = L1.ⓑ[I]V1 & Y2 = L2.ⓑ[I]V2
        | ∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I].
 /2 width=1 by rex_inv_zero_length/ qed-.