X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_lfpx.ma;h=2cfbc1a3f90c41a3090934c67644a2eb680d94cd;hb=c3832abc23bb0907df2deb6751f4a46d213675b7;hp=0c2f894b1acc8f37a16820095cd233124d911b7a;hpb=228776cd21ca563e6dc44bfdf7746e69dc7b66d6;p=helm.git

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 0c2f894b1..2cfbc1a3f 100644
--- 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