DEFINITION lt_gen_xS()
TYPE =
       ∀x:nat
         .∀n:nat
           .lt x (S n)
             →or (eq nat x O) (ex2 nat λm:nat.eq nat x (S m) λm:nat.lt m n)
BODY =
Show proof