DEFINITION well_founded_ltof()
TYPE =
       ∀A:Set.∀f:A→nat.(well_founded A (ltof A f))
BODY =
Show proof