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 =
Show proof