]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
some notation renamed and fixed
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cnx_lift.ma
index 7f3bedbd012d0436764c6d549d8de9b324d95d9f..91ea0091bc35784a63fd94dc7618e74b53d64714 100644 (file)
@@ -15,7 +15,7 @@
 include "basic_2/reduction/cpx_lift.ma".
 include "basic_2/reduction/cnx.ma".
 
-(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************)
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************)
 
 (* Relocation properties ****************************************************)