DEFINITION CTail()
TYPE =
       KTCC
BODY =
Show proof