update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma
index 5db9f7e135b12279bc5cebe5761e79c8494c3b0e..8960e8b368260b650956a2744f1ec8d6a526d966 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma
@@ -21,16 +21,16 @@ include "basic_2/rt_transition/fpbc.ma".
 
 (* Basic_2A1: uses: fpb_lpx *)
 lemma lpx_fpbc (G) (T):
-      â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â¬\88 L2 â\86\92 (L1 â\89\85[T] L2 â\86\92 â\8a¥) â\86\92 â\9dªG,L1,Tâ\9d« â\89» â\9dªG,L2,Tâ\9d«.
+      â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â¬\88 L2 â\86\92 (L1 â\89\85[T] L2 â\86\92 â\8a¥) â\86\92 â\9d¨G,L1,Tâ\9d© â\89» â\9d¨G,L2,Tâ\9d©.
 /3 width=1 by rpx_fpbc, lpx_rpx/ qed.
 
 (* Forward lemmas with extended rt-transition for full local envs ***********)
 
 lemma fpbc_fwd_lpx (G1) (G2) (L1) (L2) (T1) (T2):
-      â\9dªG1,L1,T1â\9d« â\89» â\9dªG2,L2,T2â\9d« →
-      â\88¨â\88¨ â\88\83â\88\83G,L,T. â\9dªG1,L1,T1â\9d« â¬\82 â\9dªG,L,Tâ\9d« & â\9dªG,L,Tâ\9d« â\89½ â\9dªG2,L2,T2â\9d«
-       | â\88\83â\88\83T. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88 T & T1 â\89\85 T â\86\92 â\8a¥ & â\9dªG1,L1,Tâ\9d« â\89½ â\9dªG2,L2,T2â\9d«
-       | â\88\83â\88\83L. â\9dªG1,L1â\9d« â\8a¢ â¬\88 L & (L1 â\89\85[T1] L â\86\92 â\8a¥) & â\9dªG1,L,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d«.
+      â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G2,L2,T2â\9d© →
+      â\88¨â\88¨ â\88\83â\88\83G,L,T. â\9d¨G1,L1,T1â\9d© â¬\82 â\9d¨G,L,Tâ\9d© & â\9d¨G,L,Tâ\9d© â\89½ â\9d¨G2,L2,T2â\9d©
+       | â\88\83â\88\83T. â\9d¨G1,L1â\9d© â\8a¢ T1 â¬\88 T & T1 â\89\85 T â\86\92 â\8a¥ & â\9d¨G1,L1,Tâ\9d© â\89½ â\9d¨G2,L2,T2â\9d©
+       | â\88\83â\88\83L. â\9d¨G1,L1â\9d© â\8a¢ â¬\88 L & (L1 â\89\85[T1] L â\86\92 â\8a¥) & â\9d¨G1,L,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d©.
 #G1 #G2 #L1 #L2 #T1 #T2 #H
 elim (fpbc_inv_gen sfull … H) -H #H12 #Hn12
 elim (fpb_inv_gen … H12) -H12 #L #T #H1 #HT2 #HL2