- \lambda (c1: C).(\lambda (t1: T).(\lambda (c2: C).(\lambda (t2: T).(lt
-(fweight c1 t1) (fweight c2 t2))))).
+ \lambda (c1: C).(\lambda (t1: T).(\lambda (c2: C).(\lambda (t2: T).(let
+TMP_1 \def (fweight c1 t1) in (let TMP_2 \def (fweight c2 t2) in (lt TMP_1
+TMP_2)))))).