DEFINITION asucc_gen_sort()
TYPE =
       ∀g:G
         .∀h:nat
           .∀n:nat
             .∀a:A
               .eq A (ASort h n) (asucc g a)
                 →ex_2 nat nat λh0:nat.λn0:nat.eq A a (ASort h0 n0)
BODY =
Show proof