update in basic_2 and ground_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma
index 0c2f894b1acc8f37a16820095cd233124d911b7a..44fc48fae862e8f787ed34ee71c31877b231f00c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma
@@ -13,12 +13,11 @@
 (**************************************************************************)
 
 include "basic_2/rt_computation/cpxs_lfpx.ma".
-include "basic_2/rt_computation/csx_drops.ma".
 include "basic_2/rt_computation/csx_cpxs.ma".
 
 (* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
 
-(* Advanced properties ******************************************************)
+(* Properties with uncounted parallel rt-transition on referred entries *****)
 
 (* Basic_2A1: was just: csx_lpx_conf *)
 lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
@@ -27,6 +26,8 @@ lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
 /5 width=3 by csx_intro, lfpx_cpx_trans, lfpx_cpxs_conf/
 qed-.
 
+(* Advanced properties ******************************************************)
+
 lemma csx_abst: ∀h,o,p,G,L,W. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃W⦄ →
                 ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓛ{p}W.T⦄.
 #h #o #p #G #L #W #HW @(csx_ind … HW) -W
@@ -37,7 +38,7 @@ elim (cpx_inv_abst1 … H1) -H1
 elim (tdneq_inv_pair … H2) -H2
 [ #H elim H -H //
 | -IHT #H lapply (csx_cpx_trans … o … HLT0) // -HT
-  #HT0 lapply (csx_lfpx_conf … HT0 … (L.ⓛW0)) -HT0 /4 width=1 by lfpx_pair/
+  #HT0 lapply (csx_lfpx_conf … HT0 … (L.ⓛW0)) -HT0 /4 width=1 by lfpx_pair_refl/
 | -IHW -HT /4 width=3 by csx_cpx_trans, cpx_pair_sn/
 ]
 qed.
@@ -51,7 +52,7 @@ elim (cpx_inv_abbr1 … H1) -H1 *
 [ #V1 #T1 #HLV1 #HLT1 #H destruct
   elim (tdneq_inv_pair … H2) -H2
   [ #H elim H -H //
-  | /4 width=3 by csx_cpx_trans, csx_lfpx_conf, lfpx_pair/
+  | /4 width=3 by csx_cpx_trans, csx_lfpx_conf, lfpx_pair_refl/
   | -IHV /4 width=3 by csx_cpx_trans, cpx_cpxs, cpx_pair_sn/
   ]
 | -IHV -IHT -H2
@@ -59,7 +60,7 @@ elim (cpx_inv_abbr1 … H1) -H1 *
 ]
 qed.
 
-fact csx_appl_theta_aux: â\88\80h,o,p,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Uâ¦\84 â\86\92 â\88\80V1,V2. â¬\86*[1] V1 â\89¡ V2 →
+fact csx_appl_theta_aux: â\88\80h,o,p,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Uâ¦\84 â\86\92 â\88\80V1,V2. â¬\86*[1] V1 â\89\98 V2 →
                          ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
 #h #o #p #G #L #X #H @(csx_ind_cpxs … H) -X
 #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
@@ -88,11 +89,11 @@ elim (cpx_inv_appl1 … HL) -HL *
 | -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
   lapply (cpx_lifts_bi … HLV10 (Ⓣ) … (L.ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /3 width=1 by drops_refl, drops_drop/ #HLV23
   @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
-  @(csx_lfpx_conf … (L.ⓓW0)) /2 width=1 by lfpx_pair/ -W1
+  @(csx_lfpx_conf … (L.ⓓW0)) /2 width=1 by lfpx_pair_refl/ -W1
   /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
 ]
 qed-.
 
 lemma csx_appl_theta: ∀h,o,p,G,L,V,V2,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ →
-                      â\88\80V1. â¬\86*[1] V1 â\89¡ V2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
+                      â\88\80V1. â¬\86*[1] V1 â\89\98 V2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
 /2 width=5 by csx_appl_theta_aux/ qed.