DEFINITION pc1_head()
TYPE =
       ∀u1:T.∀u2:T.(pc1 u1 u2)→∀t1:T.∀t2:T.(pc1 t1 t2)→∀k:K.(pc1 (THead k u1 t1) (THead k u2 t2))
BODY =
        assume u1: T
        assume u2: T
        suppose H: pc1 u1 u2
        assume t1: T
        assume t2: T
        suppose H0: pc1 t1 t2
        assume k: K
          (h1) 
             by (pc1_head_1 . . H . .)
pc1 (THead k u1 t1) (THead k u2 t1)
          end of h1
          (h2) 
             by (pc1_head_2 . . H0 . .)
pc1 (THead k u2 t1) (THead k u2 t2)
          end of h2
          by (pc1_t . . h1 . h2)
          we proved pc1 (THead k u1 t1) (THead k u2 t2)
       we proved ∀u1:T.∀u2:T.(pc1 u1 u2)→∀t1:T.∀t2:T.(pc1 t1 t2)→∀k:K.(pc1 (THead k u1 t1) (THead k u2 t2))