milestone update in basic_2, update in ground and static_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 0ee6c19fc33d79d6875f51a137d99d8657c9d7f6..1839df0f8a3d800c1237a3c5a005fe2ddefccad8 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
@@ -21,17 +21,17 @@ include "basic_2/rt_computation/fsb_fpbg.ma".
 
 (* Inversion lemmas with context-sensitive stringly rt-normalizing terms ****)
 
-lemma fsb_inv_csx (h):
-      ∀G,L,T. ≥𝐒[h] ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒[h] T.
-#h #G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/
+lemma fsb_inv_csx:
+      ∀G,L,T. ≥𝐒 ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒 T.
+#G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/
 qed-.
 
 (* Propreties with context-sensitive stringly rt-normalizing terms **********)
 
-lemma csx_fsb_fpbs (h):
-      ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 →
-      ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥𝐒[h] ❪G2,L2,T2❫.
-#h #G1 #L1 #T1 #H @(csx_ind … H) -T1
+lemma csx_fsb_fpbs:
+      ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
+      ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
+#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
 lapply (fpbs_csx_conf … H10) // -HT1 #HT0
@@ -58,26 +58,26 @@ generalize in match IHu; -IHu generalize in match H10; -H10
 ]
 qed.
 
-lemma csx_fsb (h):
-      ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ≥𝐒[h] ❪G,L,T❫.
+lemma csx_fsb:
+      ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → ≥𝐒 ❪G,L,T❫.
 /2 width=5 by csx_fsb_fpbs/ qed.
 
 (* Advanced eliminators *****************************************************)
 
-lemma csx_ind_fpb (h) (Q:relation3 …):
+lemma csx_ind_fpb (Q:relation3 …):
       (∀G1,L1,T1.
-        ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 →
-        (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
+        ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
+        (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) →
         Q G1 L1 T1
       ) →
-      ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → Q G L T.
+      ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
 
-lemma csx_ind_fpbg (h) (Q:relation3 …):
+lemma csx_ind_fpbg (Q:relation3 …):
       (∀G1,L1,T1.
-        ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 →
-        (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
+        ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
+        (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → Q G2 L2 T2) →
         Q G1 L1 T1
       ) →
-      ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → Q G L T.
+      ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-.