DEFINITION ex1__leq_sort_SS()
TYPE =
       ∀g:G
         .∀k:nat
           .∀n:nat
             .leq g (ASort k n) (asucc g (asucc g (ASort (S (S k)) n)))
BODY =
        assume g: G
        assume k: nat
        assume n: nat
          by (leq_refl . .)
          we proved 
             leq
               g
               asucc g (asucc g (ASort (S (S k)) n))
               asucc g (asucc g (ASort (S (S k)) n))
          that is equivalent to leq g (ASort k n) (asucc g (asucc g (ASort (S (S k)) n)))
       we proved 
          ∀g:G
            .∀k:nat
              .∀n:nat
                .leq g (ASort k n) (asucc g (asucc g (ASort (S (S k)) n)))