DEFINITION pr3_head_21()
TYPE =
       ∀c:C
         .∀u1:T.∀u2:T.(pr3 c u1 u2)→∀k:K.∀t1:T.∀t2:T.(pr3 (CHead c k u1) t1 t2)→(pr3 c (THead k u1 t1) (THead k u2 t2))
BODY =
Show proof