DEFINITION pc3_wcpr0_t()
TYPE =
       ∀c1:C.∀c2:C.(wcpr0 c1 c2)→∀t1:T.∀t2:T.(pr3 c1 t1 t2)→(pc3 c2 t1 t2)
BODY =
        assume c1: C
        assume c2: C
        suppose H: wcpr0 c1 c2
          we proceed by induction on H to prove ∀t1:T.∀t2:T.(pr3 c1 t1 t2)→(pc3 c2 t1 t2)
             case wcpr0_refl : c:C ⇒
                the thesis becomes ∀t1:T.∀t2:T.∀H0:(pr3 c t1 t2).(pc3 c t1 t2)
                    assume t1: T
                    assume t2: T
                    suppose H0: pr3 c t1 t2
                      by (pc3_pr3_r . . . H0)
                      we proved pc3 c t1 t2
∀t1:T.∀t2:T.∀H0:(pr3 c t1 t2).(pc3 c t1 t2)
             case wcpr0_comp : c0:C c3:C H0:wcpr0 c0 c3 u1:T u2:T H2:pr0 u1 u2 k:K ⇒
                the thesis becomes ∀t1:T.∀t2:T.∀H3:(pr3 (CHead c0 k u1) t1 t2).(pc3 (CHead c3 k u2) t1 t2)
                () by induction hypothesis we know ∀t1:T.∀t2:T.(pr3 c0 t1 t2)→(pc3 c3 t1 t2)
                    assume t1: T
                    assume t2: T
                    suppose H3: pr3 (CHead c0 k u1) t1 t2
                      (H4) 
                         by (pr2_free . . . H2)
                         we proved pr2 c0 u1 u2
                         by (pc3_pr2_pr3_t . . . . . H3 . previous)
pc3 (CHead c0 k u2) t1 t2
                      end of H4
                      consider H4
                      we proved pc3 (CHead c0 k u2) t1 t2
                      that is equivalent to ex2 T λt:T.pr3 (CHead c0 k u2) t1 t λt:T.pr3 (CHead c0 k u2) t2 t
                      we proceed by induction on the previous result to prove pc3 (CHead c3 k u2) t1 t2
                         case ex_intro2 : x:T H5:pr3 (CHead c0 k u2) t1 x H6:pr3 (CHead c0 k u2) t2 x ⇒
                            the thesis becomes pc3 (CHead c3 k u2) t1 t2
                               (h1) 
                                  by (pc3_wcpr0__pc3_wcpr0_t_aux . . H0 . . . . H5)
pc3 (CHead c3 k u2) t1 x
                               end of h1
                               (h2) 
                                  by (pc3_wcpr0__pc3_wcpr0_t_aux . . H0 . . . . H6)
                                  we proved pc3 (CHead c3 k u2) t2 x
                                  by (pc3_s . . . previous)
pc3 (CHead c3 k u2) x t2
                               end of h2
                               by (pc3_t . . . h1 . h2)
pc3 (CHead c3 k u2) t1 t2
                      we proved pc3 (CHead c3 k u2) t1 t2
∀t1:T.∀t2:T.∀H3:(pr3 (CHead c0 k u1) t1 t2).(pc3 (CHead c3 k u2) t1 t2)
          we proved ∀t1:T.∀t2:T.(pr3 c1 t1 t2)→(pc3 c2 t1 t2)
       we proved ∀c1:C.∀c2:C.(wcpr0 c1 c2)→∀t1:T.∀t2:T.(pr3 c1 t1 t2)→(pc3 c2 t1 t2)