DEFINITION pr2_ctail()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→∀k:K.∀u:T.(pr2 (CTail k u c) t1 t2)
BODY =
Show proof