universary milestone in basic_2

[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..31291bc3d72afaf9f858c691ee71d13f0eb3c3ab 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⦄ → ⊥.
@@ -25,16 +25,16 @@ lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 
 [ #L #K #V #i #HLK #H
   elim (cnr_inv_delta … HLK H)
 | #L #V #T #_ #IHV #H
-  elim (cnr_inv_appl … H) -H /2 width=1/
+  elim (cnr_inv_appl … H) -H /2 width=1 by/
 | #L #V #T #_ #IHT #H
-  elim (cnr_inv_appl … H) -H /2 width=1/
+  elim (cnr_inv_appl … H) -H /2 width=1 by/
 | #I #L #V #T * #H1 #H2 destruct
   [ elim (cnr_inv_zeta … H2)
-  | elim (cnr_inv_tau … H2)
+  | elim (cnr_inv_eps … H2)
   ]
 |5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
-  [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1/
-  |*: elim (cnr_inv_abst … H2) -H2 /2 width=1/
+  [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1 by/
+  |*: elim (cnr_inv_abst … H2) -H2 /2 width=1 by/
   ]
 | #a #L #V #W #T #H
   elim (cnr_inv_appl … H) -H #_ #_ #H