X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Freducibility%2Ftwhnf.ma;h=ccfaa6aa69c8b0e106ea2b7ed1501023899850d3;hb=fc7af5f9ea2cd4a876b8babc6b691136799e3c87;hp=dea7077b494eafd17e09fc2798bd20e964b3e066;hpb=9581b03be2b2bc830820b93992920aaa2c021cc9;p=helm.git

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 dea7077b4..ccfaa6aa6 100644
--- 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)"