DEFINITION ty3_nf2_inv_abst_premise_csort()
TYPE =
       ∀w:T.∀u:T.∀m:nat.(ty3_nf2_inv_abst_premise (CSort m) w u)
BODY =
Show proof