DEFINITION getl_gen_sort()
TYPE =
       ∀n:nat.∀h:nat.∀x:C.(getl h (CSort n) x)→∀P:Prop.P
BODY =
Show proof