DEFINITION pr3_head_1()
TYPE =
       ∀c:C.∀u1:T.∀u2:T.(pr3 c u1 u2)→∀k:K.∀t:T.(pr3 c (THead k u1 t) (THead k u2 t))
BODY =
        assume c: C
        assume u1: T
        assume u2: T
        suppose H: pr3 c u1 u2
          we proceed by induction on H to prove ∀k:K.∀t1:T.(pr3 c (THead k u1 t1) (THead k u2 t1))
             case pr3_refl : t:T ⇒
                the thesis becomes ∀k:K.∀t0:T.(pr3 c (THead k t t0) (THead k t t0))
                    assume k: K
                    assume t0: T
                      by (pr3_refl . .)
                      we proved pr3 c (THead k t t0) (THead k t t0)
∀k:K.∀t0:T.(pr3 c (THead k t t0) (THead k t t0))
             case pr3_sing : t2:T t1:T H0:pr2 c t1 t2 t3:T :pr3 c t2 t3 ⇒
                the thesis becomes ∀k:K.∀t:T.(pr3 c (THead k t1 t) (THead k t3 t))
                (H2) by induction hypothesis we know ∀k:K.∀t:T.(pr3 c (THead k t2 t) (THead k t3 t))
                    assume k: K
                    assume t: T
                      (h1) 
                         by (pr2_head_1 . . . H0 . .)
pr2 c (THead k t1 t) (THead k t2 t)
                      end of h1
                      (h2) 
                         by (H2 . .)
pr3 c (THead k t2 t) (THead k t3 t)
                      end of h2
                      by (pr3_sing . . . h1 . h2)
                      we proved pr3 c (THead k t1 t) (THead k t3 t)
∀k:K.∀t:T.(pr3 c (THead k t1 t) (THead k t3 t))
          we proved ∀k:K.∀t1:T.(pr3 c (THead k u1 t1) (THead k u2 t1))
       we proved ∀c:C.∀u1:T.∀u2:T.(pr3 c u1 u2)→∀k:K.∀t1:T.(pr3 c (THead k u1 t1) (THead k u2 t1))