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