more results towards the "big-tree" theorem ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / csx_aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma
index d951e4154b1c41c0f2ab2e0bd8c61961e5a550b5..43e4d3ad5a34d8806199ba51eb82f72d60d43ff9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma
@@ -17,7 +17,7 @@ include "basic_2/computation/csx_tstc_vector.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
 
-(* Main properties concerning atomic arity assignment ***********************)
+(* Main properties on atomic arity assignment *******************************)
 
 theorem aaa_csx: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
 #h #g #G #L #T #A #H