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 =
        assume c: C
        assume u1: T
        assume u2: T
        suppose H: pr3 c u1 u2
        assume k: K
        assume t1: T
        assume t2: T
        suppose H0: pr3 (CHead c k u1) t1 t2
          (h1) 
             by (pr3_head_2 . . . . . H0)
pr3 c (THead k u1 t1) (THead k u1 t2)
          end of h1
          (h2) 
             by (pr3_head_1 . . . H . .)
pr3 c (THead k u1 t2) (THead k u2 t2)
          end of h2
          by (pr3_t . . . h1 . h2)
          we proved pr3 c (THead k u1 t1) (THead k u2 t2)
       we proved 
          ∀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))