support for candidates of reducibility started ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / reducibility / tnf.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma
index a9a262efed9b6ef5a23066e547d1b71377b70dd7..5772e7626139acaf15d9a63ee2eb8f1508727f89 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma
@@ -18,8 +18,7 @@ include "Basic_2/reducibility/tpr.ma".
 
 (* CONTEXT-FREE NORMAL TERMS ************************************************)
 
-definition tnf: term → Prop ≝
-   NF … tpr (eq …).
+definition tnf: predicate term ≝ NF … tpr (eq …).
 
 interpretation
    "context-free normality (term)"