made executable again

[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 628b3b9df83b12affcd93c27593350c99a0d47ea..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,16 +24,16 @@ 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.
-#G #L #T #H @(fsb_ind_alt … H) -G -L -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-.
 
 (* 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.
-/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
+      â\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-.