DEFINITION clen()
TYPE =
       C→nat
BODY =
Show proof