DEFINITION pc1_head()
TYPE =
       ∀u1:T.∀u2:T.(pc1 u1 u2)→∀t1:T.∀t2:T.(pc1 t1 t2)→∀k:K.(pc1 (THead k u1 t1) (THead k u2 t2))
BODY =
Show proof