DEFINITION lt_wf()
TYPE =
       well_founded nat lt
BODY =
       by (well_founded_ltof . .)
       we proved well_founded nat (ltof nat λm:nat.m)
       that is equivalent to well_founded nat lt