update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / fsb_csx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
index e3ad463a62b98704bfd70ee1e04a6ea1cfa3006c..028ac11aef00e83a4818698c77ad64162704b9ad 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
@@ -24,7 +24,7 @@ include "basic_2/rt_computation/fsb_fpbg.ma".
 (* Inversion lemmas with context-sensitive stringly rt-normalizing terms ****)
 
 lemma fsb_inv_csx:
-      â\88\80G,L,T. â\89¥ð\9d\90\92 â\9dªG,L,Tâ\9d« â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 T.
+      â\88\80G,L,T. â\89¥ð\9d\90\92 â\9d¨G,L,Tâ\9d© â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 T.
 #G #L #T #H @(fsb_ind … H) -G -L -T
 /5 width=1 by csx_intro, cpx_fpbc/
 qed-.
@@ -32,8 +32,8 @@ qed-.
 (* Propreties with context-sensitive stringly rt-normalizing terms **********)
 
 lemma csx_fsb_fpbs:
-      â\88\80G1,L1,T1. â\9dªG1,L1â\9d« ⊢ ⬈*𝐒 T1 →
-      â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d« â\86\92 â\89¥ð\9d\90\92 â\9dªG2,L2,T2â\9d«.
+      â\88\80G1,L1,T1. â\9d¨G1,L1â\9d© ⊢ ⬈*𝐒 T1 →
+      â\88\80G2,L2,T2. â\9d¨G1,L1,T1â\9d© â\89¥ â\9d¨G2,L2,T2â\9d© â\86\92 â\89¥ð\9d\90\92 â\9d¨G2,L2,T2â\9d©.
 #G1 #L1 #T1 #H @(csx_ind … H) -T1
 #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind (Ⓣ) … G2 L2 T2) -G2 -L2 -T2
 #G0 #L0 #T0 #IHu #H10
@@ -64,25 +64,25 @@ elim (fpbc_fwd_lpx … H) -H * [ -IHd -IHc | -IHu -IHd |]
 qed.
 
 lemma csx_fsb (G) (L) (T):
-      â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\89¥ð\9d\90\92 â\9dªG,L,Tâ\9d«.
+      â\9d¨G,Lâ\9d© â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\89¥ð\9d\90\92 â\9d¨G,L,Tâ\9d©.
 /2 width=5 by csx_fsb_fpbs/ qed.
 
 (* Advanced eliminators *****************************************************)
 
 lemma csx_ind_fpbc (Q:relation3 …):
       (∀G1,L1,T1.
-        â\9dªG1,L1â\9d« ⊢ ⬈*𝐒 T1 →
-        (â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« â\89» â\9dªG2,L2,T2â\9d« → Q G2 L2 T2) →
+        â\9d¨G1,L1â\9d© ⊢ ⬈*𝐒 T1 →
+        (â\88\80G2,L2,T2. â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G2,L2,T2â\9d© → Q G2 L2 T2) →
         Q G1 L1 T1
       ) →
-      â\88\80G,L,T. â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 T → Q G L T.
+      â\88\80G,L,T. â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 T → Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind/ qed-.
 
 lemma csx_ind_fpbg (Q:relation3 …):
       (∀G1,L1,T1.
-        â\9dªG1,L1â\9d« ⊢ ⬈*𝐒 T1 →
-        (â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d« → Q G2 L2 T2) →
+        â\9d¨G1,L1â\9d© ⊢ ⬈*𝐒 T1 →
+        (â\88\80G2,L2,T2. â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d© → Q G2 L2 T2) →
         Q G1 L1 T1
       ) →
-      â\88\80G,L,T. â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 T → Q G L T.
+      â\88\80G,L,T. â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 T → Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-.