support for candidates of reducibility started ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / grammar / cl_weight.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
index 355b8a7973a46bbcd67c4093df77939cbc2a9b0f..0414499a59de0aee49a610b8bf83394a6388d970 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
@@ -26,7 +26,7 @@ interpretation "weight (closure)" 'Weight L T = (cw L T).
 (* Basic_1: was: flt_wf__q_ind *)
 
 (* Basic_1: was: flt_wf_ind *)
-axiom cw_wf_ind: ∀R:lenv→term→Prop.
+axiom cw_wf_ind: ∀R:lenv→predicate term.
                  (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → R L1 T1) → R L2 T2) →
                  ∀L,T. R L T.