DEFINITION tlt()
TYPE =
T
→
T
→
Prop
BODY =
λ
t1:
T
.
λ
t2:
T
.
lt
(
weight
t1) (
weight
t2)