| (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.