DEFINITION pr1_head_1()
TYPE =
       ∀u1:T.∀u2:T.(pr1 u1 u2)→∀t:T.∀k:K.(pr1 (THead k u1 t) (THead k u2 t))
BODY =
Show proof