DEFINITION pc3_head_1()
TYPE =
       ∀c:C.∀u1:T.∀u2:T.(pc3 c u1 u2)→∀k:K.∀t:T.(pc3 c (THead k u1 t) (THead k u2 t))
BODY =
        assume c: C
        assume u1: T
        assume u2: T
        suppose H: pc3 c u1 u2
        assume k: K
        assume t: T
          (H0) consider H
          consider H0
          we proved pc3 c u1 u2
          that is equivalent to ex2 T λt0:T.pr3 c u1 t0 λt0:T.pr3 c u2 t0
          we proceed by induction on the previous result to prove pc3 c (THead k u1 t) (THead k u2 t)
             case ex_intro2 : x:T H1:pr3 c u1 x H2:pr3 c u2 x ⇒
                the thesis becomes pc3 c (THead k u1 t) (THead k u2 t)
                   (h1) 
                      by (pr3_refl . .)
                      we proved pr3 (CHead c k x) t t
                      by (pr3_head_12 . . . H1 . . . previous)
pr3 c (THead k u1 t) (THead k x t)
                   end of h1
                   (h2) 
                      by (pr3_refl . .)
                      we proved pr3 (CHead c k x) t t
                      by (pr3_head_12 . . . H2 . . . previous)
pr3 c (THead k u2 t) (THead k x t)
                   end of h2
                   by (ex_intro2 . . . . h1 h2)
                   we proved ex2 T λt0:T.pr3 c (THead k u1 t) t0 λt0:T.pr3 c (THead k u2 t) t0
pc3 c (THead k u1 t) (THead k u2 t)
          we proved pc3 c (THead k u1 t) (THead k u2 t)
       we proved ∀c:C.∀u1:T.∀u2:T.(pc3 c u1 u2)→∀k:K.∀t:T.(pc3 c (THead k u1 t) (THead k u2 t))