update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lpx.ma
index 2aa0f0d4d2a19975e0b2db2087dc77ead2ed51ad..3010a96ca5a1537514ed2c3020c1591bf592ae53 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lpx.ma
@@ -21,19 +21,19 @@ include "basic_2/rt_transition/fpb.ma".
 
 (* Basic_2A1: uses: fpbq_lpx *)
 lemma lpx_fpb (G) (T):
-      â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â¬\88 L2 â\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 â\9d¨G,L1,Tâ\9d© â\89½ â\9d¨G,L2,Tâ\9d©.
 /3 width=1 by rpx_fpb, lpx_rpx/ qed.
 
 lemma fpb_intro_req (G1) (G2) (L1) (L2) (T1) (T2):
-      â\88\80L0,L,T. â\9dªG1,L1,T1â\9d« â¬\82⸮ â\9dªG2,L,Tâ\9d« â\86\92 â\9dªG2,Lâ\9d« ⊢ T ⬈ T2 → 
-      L â\89¡[T] L0 â\86\92 â\9dªG2,L0â\9d« â\8a¢ â¬\88 L2 â\86\92 â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d«.
+      â\88\80L0,L,T. â\9d¨G1,L1,T1â\9d© â¬\82⸮ â\9d¨G2,L,Tâ\9d© â\86\92 â\9d¨G2,Lâ\9d© ⊢ T ⬈ T2 → 
+      L â\89¡[T] L0 â\86\92 â\9d¨G2,L0â\9d© â\8a¢ â¬\88 L2 â\86\92 â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d©.
 /4 width=10 by fpb_intro, lpx_rpx, reqg_rpx_trans/ qed.
 
 (* Inversion lemmas with extended rt-transition for full local envs *********)
 
 lemma fpb_inv_req (G1) (G2) (L1) (L2) (T1) (T2):
-      â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d« →
-      â\88\83â\88\83L0,L,T. â\9dªG1,L1,T1â\9d« â¬\82⸮ â\9dªG2,L,Tâ\9d« & â\9dªG2,Lâ\9d« â\8a¢ T â¬\88 T2 & L â\89¡[T] L0 & â\9dªG2,L0â\9d« ⊢ ⬈ L2.
+      â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d© →
+      â\88\83â\88\83L0,L,T. â\9d¨G1,L1,T1â\9d© â¬\82⸮ â\9d¨G2,L,Tâ\9d© & â\9d¨G2,Lâ\9d© â\8a¢ T â¬\88 T2 & L â\89¡[T] L0 & â\9d¨G2,L0â\9d© ⊢ ⬈ L2.
 #G1 #G2 #L1 #L2 #T1 #T2 * #L #T #H1 #HT2 #HL2
 elim (rpx_inv_req_lpx … HL2) -HL2 #L0 #HL0 #HL02
 /2 width=7 by ex4_3_intro/
@@ -42,8 +42,8 @@ qed-.
 (* Forward lemmas with extended rt-transition for full local envs ***********)
 
 lemma fpb_fwd_req (G1) (G2) (L1) (L2) (T1) (T2):
-      â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d« →
-      â\88\83â\88\83L0,L,T. â\9dªG1,L1,T1â\9d« â¬\82⸮ â\9dªG2,L,Tâ\9d« & â\9dªG2,Lâ\9d« â\8a¢ T â¬\88 T2 & â\9dªG2,Lâ\9d« ⊢ ⬈ L0 & L0 ≡[T] L2.
+      â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d© →
+      â\88\83â\88\83L0,L,T. â\9d¨G1,L1,T1â\9d© â¬\82⸮ â\9d¨G2,L,Tâ\9d© & â\9d¨G2,Lâ\9d© â\8a¢ T â¬\88 T2 & â\9d¨G2,Lâ\9d© ⊢ ⬈ L0 & L0 ≡[T] L2.
 #G1 #G2 #L1 #L2 #T1 #T2 * #L #T #H1 #HT2 #HL2
 elim (rpx_fwd_lpx_req … HL2) -HL2 #L0 #HL0 #HL02
 /2 width=7 by ex4_3_intro/