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