DEFINITION pr1_head_1()
TYPE =
       ∀u1:T.∀u2:T.(pr1 u1 u2)→∀t:T.∀k:K.(pr1 (THead k u1 t) (THead k u2 t))
BODY =
        assume u1: T
        assume u2: T
        suppose H: pr1 u1 u2
        assume t: T
        assume k: K
          we proceed by induction on H to prove pr1 (THead k u1 t) (THead k u2 t)
             case pr1_refl : t0:T ⇒
                the thesis becomes pr1 (THead k t0 t) (THead k t0 t)
                   by (pr1_refl .)
pr1 (THead k t0 t) (THead k t0 t)
             case pr1_sing : t2:T t1:T H0:pr0 t1 t2 t3:T :pr1 t2 t3 ⇒
                the thesis becomes pr1 (THead k t1 t) (THead k t3 t)
                (H2) by induction hypothesis we know pr1 (THead k t2 t) (THead k t3 t)
                   by (pr0_refl .)
                   we proved pr0 t t
                   by (pr0_comp . . H0 . . previous .)
                   we proved pr0 (THead k t1 t) (THead k t2 t)
                   by (pr1_sing . . previous . H2)
pr1 (THead k t1 t) (THead k t3 t)
          we proved pr1 (THead k u1 t) (THead k u2 t)
       we proved ∀u1:T.∀u2:T.(pr1 u1 u2)→∀t:T.∀k:K.(pr1 (THead k u1 t) (THead k u2 t))