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