DEFINITION pr2_head_1()
TYPE =
       ∀c:C.∀u1:T.∀u2:T.(pr2 c u1 u2)→∀k:K.∀t:T.(pr2 c (THead k u1 t) (THead k u2 t))
BODY =
Show proof