DEFINITION lt_wf_ind()
TYPE =
       ∀p:nat
         .∀P:nat→Prop
           .(∀n:nat.(∀m:nat.(lt m n)→(P m))→(P n))→(P p)
BODY =
        assume p: nat
        assume P: nat→Prop
        suppose H: ∀n:nat.(∀m:nat.(lt m n)→(P m))→(P n)
          by (lt_wf .)
          we proved Acc nat lt p
          we proceed by induction on the previous result to prove P p
             case Acc_intro : x:nat :∀y:nat.(lt y x)→(Acc nat lt y) ⇒
                the thesis becomes P x
                (H1) by induction hypothesis we know ∀y:nat.(lt y x)→(P y)
                   by (H . H1)
P x
          we proved P p
       we proved 
          ∀p:nat
            .∀P:nat→Prop
              .(∀n:nat.(∀m:nat.(lt m n)→(P m))→(P n))→(P p)