DEFINITION le_Sx_x()
TYPE =
       ∀x:nat.(le (S x) x)→∀P:Prop.P
BODY =
        assume x: nat
        suppose H: le (S x) x
        assume P: Prop
          (H0) consider le_Sn_n
          by (H0 . H)
          we proved False
          we proceed by induction on the previous result to prove P
          we proved P
       we proved ∀x:nat.(le (S x) x)→∀P:Prop.P