- support for candidates of reducibility continues ...

[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 915b17288f96980ffd8681c6d2c37dd9708bdfaf..5dadd06deed5da57084a7397f05ae6afc443bfaf 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
@@ -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).