DEFINITION pc3_head_2()
TYPE =
       ∀c:C.∀u:T.∀t1:T.∀t2:T.∀k:K.(pc3 (CHead c k u) t1 t2)→(pc3 c (THead k u t1) (THead k u t2))
BODY =
Show proof