update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma
index 9d9af6c964e232c6c43eb1e11ffea4c3053e7dbb..245c10f530c4917564ed1e7be2dac1763370d2d9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma
@@ -20,7 +20,7 @@ include "basic_2/rt_transition/rpx.ma".
 
 (* Basic_2A1: uses: fpbq *)
 definition fpb (G1) (L1) (T1) (G2) (L2) (T2): Prop ≝
-           â\88\83â\88\83L,T. â\9dªG1,L1,T1â\9d« â¬\82⸮ â\9dªG2,L,Tâ\9d« & â\9dªG2,Lâ\9d« â\8a¢ T â¬\88 T2 & â\9dªG2,Lâ\9d« ⊢ ⬈[T] L2.
+           â\88\83â\88\83L,T. â\9d¨G1,L1,T1â\9d© â¬\82⸮ â\9d¨G2,L,Tâ\9d© & â\9d¨G2,Lâ\9d© â\8a¢ T â¬\88 T2 & â\9d¨G2,Lâ\9d© ⊢ ⬈[T] L2.
 
 interpretation
   "parallel rst-transition (closure)"
@@ -29,19 +29,19 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma fpb_intro (G1) (L1) (T1) (G2) (L2) (T2):
-      â\88\80L,T. â\9dªG1,L1,T1â\9d« â¬\82⸮ â\9dªG2,L,Tâ\9d« â\86\92 â\9dªG2,Lâ\9d« ⊢ T ⬈ T2 → 
-      â\9dªG2,Lâ\9d« â\8a¢ â¬\88[T] L2 â\86\92 â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d«.
+      â\88\80L,T. â\9d¨G1,L1,T1â\9d© â¬\82⸮ â\9d¨G2,L,Tâ\9d© â\86\92 â\9d¨G2,Lâ\9d© ⊢ T ⬈ T2 → 
+      â\9d¨G2,Lâ\9d© â\8a¢ â¬\88[T] L2 â\86\92 â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d©.
 /2 width=5 by ex3_2_intro/ qed.
 
 lemma rpx_fpb (G) (T):
-      â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â¬\88[T] L2 â\86\92 â\9dªG,L1,Tâ\9d« â\89½ â\9dªG,L2,Tâ\9d«.
+      â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â¬\88[T] L2 â\86\92 â\9d¨G,L1,Tâ\9d© â\89½ â\9d¨G,L2,Tâ\9d©.
 /2 width=5 by fpb_intro/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
 lemma fpb_inv_gen (G1) (L1) (T1) (G2) (L2) (T2):
-      â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d« →
-      â\88\83â\88\83L,T. â\9dªG1,L1,T1â\9d« â¬\82⸮ â\9dªG2,L,Tâ\9d« & â\9dªG2,Lâ\9d« â\8a¢ T â¬\88 T2 & â\9dªG2,Lâ\9d« ⊢ ⬈[T] L2.
+      â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d© →
+      â\88\83â\88\83L,T. â\9d¨G1,L1,T1â\9d© â¬\82⸮ â\9d¨G2,L,Tâ\9d© & â\9d¨G2,Lâ\9d© â\8a¢ T â¬\88 T2 & â\9d¨G2,Lâ\9d© ⊢ ⬈[T] L2.
 // qed-.
 
 (* Basic_2A1: removed theorems 2: