DEFINITION ltof()
TYPE =
Π
A:
Set
.(A
→
nat
)
→
A
→
A
→
Prop
BODY =
λ
A:
Set
.
λ
f:A
→
nat
.
λ
a:A.
λ
b:A.
lt
(f a) (f b)