X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2Ftlt_defs.ma;h=390c067cc15823721e09fdf7f81653f2f1e2a9c1;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1d5f73f17b01283028da43a233572ae7e6c6bb46;hpb=1e7db0c9a71cb3720d36ab090706a84e3f539fe0;p=helm.git

diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
index 1d5f73f17..390c067cc 100644
--- a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
@@ -44,6 +44,10 @@ let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T A N) on t : nat \def
       | (TGRef y n)     \Rightarrow O
   ].
 
-definition weight : \forall A,N. T A N \to nat \def \lambda A,N.(weight_map A N (\lambda _.O)).
+definition weight: \forall A,N. T A N \to nat \def 
+   \lambda A,N. 
+   (weight_map A N (\lambda _.O)).
 
-definition tlt : \forall A,N. T A N \to T A N \to Prop \def \lambda A,N. \lambda t1,t2. weight A N t1 < weight A N t2.
+definition tlt: \forall A,N. T A N \to T A N \to Prop \def 
+   \lambda A,N,t1,t2. 
+   weight A N t1 < weight A N t2.