X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcnr_crr.ma;h=35937fb419baac44a98bc2821415f97dbac8d4a1;hb=a76f56fdad6348b167376093920650379c9936d4;hp=c72c3315e14669c794baa8533dd53a84269e8813;hpb=606dab57f31b66eb3f30f603185124b88dfad4c1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
index c72c3315e..35937fb41 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
@@ -15,9 +15,9 @@
 include "basic_2/reduction/crr.ma".
 include "basic_2/reduction/cnr.ma".
 
-(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************)
 
-(* Advanced inversion lemmas on context-sensitive reducible terms ***********)
+(* Advanced inversion lemmas on reducibility ********************************)
 
 (* Note: this property is unusual *)
 lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → ⊥.