DEFINITION pc1_head_2()
TYPE =
       ∀t1:T.∀t2:T.(pc1 t1 t2)→∀u:T.∀k:K.(pc1 (THead k u t1) (THead k u t2))
BODY =
Show proof