DEFINITION llt()
TYPE =
A
→
A
→
Prop
BODY =
λ
a1:
A
.
λ
a2:
A
.
lt
(
lweight
a1) (
lweight
a2)