X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_cnx_vector.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_cnx_vector.ma;h=fbaee7c73c2f0ac70b50bb0e3057e902d4e472ef;hb=b4283c079ed7069016b8d924bbc7e08872440829;hp=91a7f292512e17d40b358af5e5f8278a5faf35f4;hpb=647b419e96770d90a82d7a9e5e8843566a9f93ee;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
index 91a7f2925..fbaee7c73 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
@@ -38,5 +38,6 @@ qed.
 
 (* Advanced properties ******************************************************)
 
+(* Note: strong normalization does not depend on this any more *)
 lemma csx_applv_sort: ∀h,G,L,s,Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.⋆s⦄.
 /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed.