DEFINITION nf2_sort()
TYPE =
∀
c:
C
.
∀
n:
nat
.(
nf2
c (
TSort
n))
BODY =
Show proof