DEFINITION csubst0_gen_sort()
TYPE =
       ∀x:C.∀v:T.∀i:nat.∀n:nat.(csubst0 i v (CSort n) x)→∀P:Prop.P
BODY =
Show proof