DEFINITION pc3_pr3_pc3_t()
TYPE =
       ∀c:C.∀u1:T.∀u2:T.(pr3 c u2 u1)→∀t1:T.∀t2:T.∀k:K.(pc3 (CHead c k u2) t1 t2)→(pc3 (CHead c k u1) t1 t2)
BODY =
        assume c: C
        assume u1: T
        assume u2: T
        suppose H: pr3 c u2 u1
          we proceed by induction on H to prove ∀t1:T.∀t2:T.∀k:K.(pc3 (CHead c k u2) t1 t2)→(pc3 (CHead c k u1) t1 t2)
             case pr3_refl : t:T ⇒
                    assume t1: T
                    assume t2: T
                    assume k: K
                    suppose H0: pc3 (CHead c k t) t1 t2
                      consider H0
             case pr3_sing : t2:T t1:T H0:pr2 c t1 t2 t3:T :pr3 c t2 t3 ⇒
                the thesis becomes ∀t0:T.∀t4:T.∀k:K.∀H3:(pc3 (CHead c k t1) t0 t4).(pc3 (CHead c k t3) t0 t4)
                (H2) by induction hypothesis we know ∀t4:T.∀t5:T.∀k:K.(pc3 (CHead c k t2) t4 t5)→(pc3 (CHead c k t3) t4 t5)
                    assume t0: T
                    assume t4: T
                    assume k: K
                    suppose H3: pc3 (CHead c k t1) t0 t4
                      (H4) consider H3
                      consider H4
                      we proved pc3 (CHead c k t1) t0 t4
                      that is equivalent to ex2 T λt:T.pr3 (CHead c k t1) t0 t λt:T.pr3 (CHead c k t1) t4 t
                      we proceed by induction on the previous result to prove pc3 (CHead c k t2) t0 t4
                         case ex_intro2 : x:T H5:pr3 (CHead c k t1) t0 x H6:pr3 (CHead c k t1) t4 x ⇒
                            the thesis becomes pc3 (CHead c k t2) t0 t4
                               (h1) 
                                  by (pc3_pr2_pr3_t . . . . . H5 . H0)
pc3 (CHead c k t2) t0 x
                               end of h1
                               (h2) 
                                  by (pc3_pr2_pr3_t . . . . . H6 . H0)
                                  we proved pc3 (CHead c k t2) t4 x
                                  by (pc3_s . . . previous)
pc3 (CHead c k t2) x t4
                               end of h2
                               by (pc3_t . . . h1 . h2)
pc3 (CHead c k t2) t0 t4
                      we proved pc3 (CHead c k t2) t0 t4
                      by (H2 . . . previous)
                      we proved pc3 (CHead c k t3) t0 t4
∀t0:T.∀t4:T.∀k:K.∀H3:(pc3 (CHead c k t1) t0 t4).(pc3 (CHead c k t3) t0 t4)
          we proved ∀t1:T.∀t2:T.∀k:K.(pc3 (CHead c k u2) t1 t2)→(pc3 (CHead c k u1) t1 t2)
       we proved ∀c:C.∀u1:T.∀u2:T.(pr3 c u2 u1)→∀t1:T.∀t2:T.∀k:K.(pc3 (CHead c k u2) t1 t2)→(pc3 (CHead c k u1) t1 t2)