DEFINITION pr2_head_2()
TYPE =
       ∀c:C.∀u:T.∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u) t1 t2)→(pr2 c (THead k u t1) (THead k u t2))
BODY =
Show proof