- first properties of strongly normalizing terms

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / computation / csn_cr.ma

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 5dadd06deed5da57084a7397f05ae6afc443bfaf..bbdfd773ef4cfdec8377d0821426ae0fb35ac813 100644 (file)
--- 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 â\80¦) (csn â\80¦) (λL,T. L â\8a¢ â\87\93 T).
+axiom csn_acr: acr cpr (eq â\80¦) (csn â\80¦) (λL,T. L â\8a¢ â¬\87* T).