DEFINITION drop_gen_sort()
TYPE =
       ∀n:nat
         .∀h:nat
           .∀d:nat
             .∀x:C
               .drop h d (CSort n) x
                 →and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O)
BODY =
Show proof