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