DEFINITION ltof()
TYPE =
Π
A:
Set
.(A
→
nat
)
→
A
→
A
→
Prop
BODY =
Show proof