update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma
index 845fc6d276bbc890def968b825524563e1327cbd..54202be4aeb5b939bfc7de9c7b76e591880b2ea5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma
@@ -21,25 +21,25 @@ include "basic_2/rt_transition/lpx.ma".
 (* Properties with syntactic equivalence for referred local environments ****)
 
 lemma req_rpx (G) (T):
-      â\88\80L1,L2. L1 â\89¡[T] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[T] L2.
+      â\88\80L1,L2. L1 â\89¡[T] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
 /2 width=1 by req_fwd_rex/ qed.
 
 (* Properties with extended rt-transition for full local envs ***************)
 
 lemma lpx_rpx (G) (T):
-      â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â¬\88 L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[T] L2.
+      â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â¬\88 L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
 /2 width=1 by rex_lex/ qed.
 
 (* Inversion lemmas with extended rt-transition for full local envs *********)
 
 lemma rpx_inv_req_lpx (G) (T):
-      â\88\80L1,L2. â\9dªG,L1â\9d« ⊢ ⬈[T] L2 →
-      â\88\83â\88\83L. L1 â\89¡[T] L & â\9dªG,Lâ\9d« ⊢ ⬈ L2.
+      â\88\80L1,L2. â\9d¨G,L1â\9d© ⊢ ⬈[T] L2 →
+      â\88\83â\88\83L. L1 â\89¡[T] L & â\9d¨G,Lâ\9d© ⊢ ⬈ L2.
 /4 width=13 by cpx_reqg_conf, rex_inv_req_lex, rex_conf1_next/ qed-.
 
 (* Forward lemmas with extended rt-transition for full local envs ***********)
 
 lemma rpx_fwd_lpx_req (G) (T):
-      â\88\80L1,L2. â\9dªG,L1â\9d« ⊢ ⬈[T] L2 →
-      â\88\83â\88\83L. â\9dªG,L1â\9d« ⊢ ⬈ L & L ≡[T] L2.
+      â\88\80L1,L2. â\9d¨G,L1â\9d© ⊢ ⬈[T] L2 →
+      â\88\83â\88\83L. â\9d¨G,L1â\9d© ⊢ ⬈ L & L ≡[T] L2.
 /3 width=3 by rpx_fsge_comp, rex_fwd_lex_req/ qed-.