X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn_cr.ma;h=bbdfd773ef4cfdec8377d0821426ae0fb35ac813;hb=b5db76fe31ab35bae0257cb6684c511bcc531e45;hp=5dadd06deed5da57084a7397f05ae6afc443bfaf;hpb=0aa60d67f17b528b896e05bbd01038cbc195f69d;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
index 5dadd06de..bbdfd773e 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
@@ -13,10 +13,10 @@
 (**************************************************************************)
 
 include "Basic_2/computation/acp_cr.ma".
-include "Basic_2/computation/csn.ma".
+include "Basic_2/computation/csn_lift.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
 
 (* Advanced properties ******************************************************)
 
-axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⇓ T).
+axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T).