X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_csx_vector.ma;h=30f35f70fef5a1de10d690f9e4fbaf2d6b9cc9dd;hb=5c92c318030a05c766b3f6070dbd23589cbdee04;hp=e1166a0fd127622a1319dfd8125516b58367b251;hpb=397413c4196f84c81d61ba7dd79b54ab1c428ebb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
index e1166a0fd..30f35f70f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
@@ -15,10 +15,10 @@
 include "basic_2/rt_computation/cpxs_theq_vector.ma".
 include "basic_2/rt_computation/csx_simple_theq.ma".
 include "basic_2/rt_computation/csx_lsubr.ma".
-include "basic_2/rt_computation/csx_lfpx.ma".
+include "basic_2/rt_computation/csx_lpx.ma".
 include "basic_2/rt_computation/csx_vector.ma".
 
-(* STRONGLY NORMALIZING TERM VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION ***)
+(* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****)
 
 (* Advanced properties ************************************* ****************)
 
@@ -67,7 +67,7 @@ lapply (csx_appl_theta … H … HW12) -H -HW12 #H
 lapply (csx_fwd_pair_sn … H) #HW1
 lapply (csx_fwd_flat_dx … H) #H1
 @csx_appl_simple_theq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
-elim (cpxs_fwd_theta_vector … o … (V2@V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
+elim (cpxs_fwd_theta_vector … o … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
 [ -H #H elim H2 -H2 //
 | -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
 ]