DEFINITION pc3_dec()
TYPE =
       ∀g:G.∀c:C.∀u1:T.∀t1:T.(ty3 g c u1 t1)→∀u2:T.∀t2:T.(ty3 g c u2 t2)→(or (pc3 c u1 u2) (pc3 c u1 u2)→False)
BODY =
        assume g: G
        assume c: C
        assume u1: T
        assume t1: T
        suppose H: ty3 g c u1 t1
        assume u2: T
        assume t2: T
        suppose H0: ty3 g c u2 t2
          (H_y) by (ty3_sn3 . . . . H) we proved sn3 c u1
          (H_y0) by (ty3_sn3 . . . . H0) we proved sn3 c u2
          (H_x) 
             by (nf2_sn3 . . H_y)
ex2 T λu:T.pr3 c u1 u λu:T.nf2 c u
          end of H_x
          (H1) consider H_x
          we proceed by induction on H1 to prove or (pc3 c u1 u2) (pc3 c u1 u2)→False
             case ex_intro2 : x:T H2:pr3 c u1 x H3:nf2 c x ⇒
                the thesis becomes or (pc3 c u1 u2) (pc3 c u1 u2)→False
                   (H_x0) 
                      by (nf2_sn3 . . H_y0)
ex2 T λu:T.pr3 c u2 u λu:T.nf2 c u
                   end of H_x0
                   (H4) consider H_x0
                   we proceed by induction on H4 to prove or (pc3 c u1 u2) (pc3 c u1 u2)→False
                      case ex_intro2 : x0:T H5:pr3 c u2 x0 H6:nf2 c x0 ⇒
                         the thesis becomes or (pc3 c u1 u2) (pc3 c u1 u2)→False
                            (H_x1) 
                               by (term_dec . .)
or (eq T x x0) (eq T x x0)→∀P:Prop.P
                            end of H_x1
                            (H7) consider H_x1
                            we proceed by induction on H7 to prove or (pc3 c u1 u2) (pc3 c u1 u2)→False
                               case or_introl : H8:eq T x x0 ⇒
                                  the thesis becomes or (pc3 c u1 u2) (pc3 c u1 u2)→False
                                     (H10) 
                                        by (eq_ind_r . . . H5 . H8)
pr3 c u2 x
                                     end of H10
                                     by (pc3_pr3_t . . . H2 . H10)
                                     we proved pc3 c u1 u2
                                     by (or_introl . . previous)
or (pc3 c u1 u2) (pc3 c u1 u2)→False
                               case or_intror : H8:(eq T x x0)→∀P:Prop.P ⇒
                                  the thesis becomes or (pc3 c u1 u2) (pc3 c u1 u2)→False
                                     suppose H9: pc3 c u1 u2
                                        (H10) consider H9
                                        consider H10
                                        we proved pc3 c u1 u2
                                        that is equivalent to ex2 T λt:T.pr3 c u1 t λt:T.pr3 c u2 t
                                        we proceed by induction on the previous result to prove False
                                           case ex_intro2 : x1:T H11:pr3 c u1 x1 H12:pr3 c u2 x1 ⇒
                                              the thesis becomes False
                                                 (H_x2) 
                                                    by (pr3_confluence . . . H5 . H12)
ex2 T λt:T.pr3 c x0 t λt:T.pr3 c x1 t
                                                 end of H_x2
                                                 (H13) consider H_x2
                                                 we proceed by induction on H13 to prove False
                                                    case ex_intro2 : x2:T H14:pr3 c x0 x2 H15:pr3 c x1 x2 ⇒
                                                       the thesis becomes False
                                                          (H_y1) 
                                                             by (nf2_pr3_unfold . . . H14 H6)
eq T x0 x2
                                                          end of H_y1
                                                          (H16) 
                                                             by (eq_ind_r . . . H15 . H_y1)
pr3 c x1 x0
                                                          end of H16
                                                          (H17) 
                                                             by (nf2_pr3_confluence . . H3 . H6 . H2)
(pr3 c u1 x0)→(eq T x x0)
                                                          end of H17
                                                          by (pr3_t . . . H11 . H16)
                                                          we proved pr3 c u1 x0
                                                          by (H17 previous)
                                                          we proved eq T x x0
                                                          by (H8 previous .)
False
False
                                        we proved False
                                     we proved (pc3 c u1 u2)→False
                                     by (or_intror . . previous)
or (pc3 c u1 u2) (pc3 c u1 u2)→False
or (pc3 c u1 u2) (pc3 c u1 u2)→False
or (pc3 c u1 u2) (pc3 c u1 u2)→False
          we proved or (pc3 c u1 u2) (pc3 c u1 u2)→False
       we proved ∀g:G.∀c:C.∀u1:T.∀t1:T.(ty3 g c u1 t1)→∀u2:T.∀t2:T.(ty3 g c u2 t2)→(or (pc3 c u1 u2) (pc3 c u1 u2)→False)