- more properties on strongly normalizing terms

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

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma
index ace3b9feab2764fcb41615cc2508e783744b46d2..4a936f607864a36067ed488aa7b4bdc18ea1ebdb 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma
@@ -25,10 +25,6 @@ interpretation
    "context-sensitive strong normalization (term)"
    'SNStar L T = (csns L T).
 
-notation "hvbox( L ⊢ ⬇ * * T )"
-   non associative with precedence 45
-   for @{ 'SNStar $L $T }.
-
 (* Basic eliminators ********************************************************)
 
 lemma csns_ind: ∀L. ∀R:predicate term.