DEFINITION pr1_comp()
TYPE =
       ∀v:T.∀w:T.(pr1 v w)→∀t:T.∀u:T.(pr1 t u)→∀k:K.(pr1 (THead k v t) (THead k w u))
BODY =
Show proof