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