DEFINITION nf2_csort_lref()
TYPE =
       ∀n:nat.∀i:nat.(nf2 (CSort n) (TLRef i))
BODY =
Show proof