DEFINITION lt_wf()
TYPE =
       well_founded nat lt
BODY =
Show proof