some notation renamed and fixed

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cnr_crr.ma

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 c72c3315e14669c794baa8533dd53a84269e8813..35937fb419baac44a98bc2821415f97dbac8d4a1 100644 (file)
--- 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⦄ → ⊥.