DEFINITION aprem_gen_sort()
TYPE =
       ∀x:A.∀i:nat.∀h:nat.∀n:nat.(aprem i (ASort h n) x)→False
BODY =
Show proof