X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fgrammar%2Fcl_weight.ma;h=0414499a59de0aee49a610b8bf83394a6388d970;hb=fc7af5f9ea2cd4a876b8babc6b691136799e3c87;hp=355b8a7973a46bbcd67c4093df77939cbc2a9b0f;hpb=04f6ca789cac88220234a3bdfb497844c417ef14;p=helm.git

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 355b8a797..0414499a5 100644
--- 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.