additions and corrections for the article on λδ-2B

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

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 91a7f292512e17d40b358af5e5f8278a5faf35f4..fbaee7c73c2f0ac70b50bb0e3057e902d4e472ef 100644 (file)
--- 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.