support for candidates of reducibility started ...

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

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma
index dea7077b494eafd17e09fc2798bd20e964b3e066..ccfaa6aa69c8b0e106ea2b7ed1501023899850d3 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma
@@ -17,8 +17,7 @@ include "Basic_2/reducibility/tpr.ma".
 
 (* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
 
-definition twhnf: term → Prop ≝
-   NF … tpr thom.
+definition twhnf: predicate term ≝ NF … tpr thom.
 
 interpretation
    "context-free weak head normality (term)"