X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn_cr.ma;h=98a8db1deabd125f4b6849cc63d619c1fb623735;hb=720637242f8c46adef24da44f29129faa09469de;hp=915b17288f96980ffd8681c6d2c37dd9708bdfaf;hpb=35653f628dc3a3e665fee01acc19c660c9d555e3;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 915b17288..98a8db1de 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
@@ -17,9 +17,6 @@ include "Basic_2/computation/csn.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
 
-(* the candidate of reducibility associated to an atomic arity *)
-definition snc: aarity → lenv → predicate term ≝ acr csn.
+(* Advanced properties ******************************************************)
 
-interpretation
-   "candidate of reducibility (contex-sensitive strong normalization)"
-   'InEInt L T A = (snc A L T).
+axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T).