DEFINITION lt_wf_ind()
TYPE =
       ∀p:nat
         .∀P:nat→Prop
           .(∀n:nat.(∀m:nat.(lt m n)→(P m))→(P n))→(P p)
BODY =
Show proof