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