DEFINITION pr3_confluence()
TYPE =
       ∀c:C.∀t0:T.∀t1:T.(pr3 c t0 t1)→∀t2:T.(pr3 c t0 t2)→(ex2 T λt:T.pr3 c t1 t λt:T.pr3 c t2 t)
BODY =
        assume c: C
        assume t0: T
        assume t1: T
        suppose H: pr3 c t0 t1
          we proceed by induction on H to prove ∀t3:T.(pr3 c t0 t3)→(ex2 T λt4:T.pr3 c t1 t4 λt4:T.pr3 c t3 t4)
             case pr3_refl : t:T ⇒
                the thesis becomes ∀t2:T.∀H0:(pr3 c t t2).(ex2 T λt3:T.pr3 c t t3 λt3:T.pr3 c t2 t3)
                    assume t2: T
                    suppose H0: pr3 c t t2
                      by (pr3_refl . .)
                      we proved pr3 c t2 t2
                      by (ex_intro2 . . . . H0 previous)
                      we proved ex2 T λt3:T.pr3 c t t3 λt3:T.pr3 c t2 t3
∀t2:T.∀H0:(pr3 c t t2).(ex2 T λt3:T.pr3 c t t3 λt3:T.pr3 c t2 t3)
             case pr3_sing : t2:T t3:T H0:pr2 c t3 t2 t4:T :pr3 c t2 t4 ⇒
                the thesis becomes ∀t5:T.∀H3:(pr3 c t3 t5).(ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t)
                (H2) by induction hypothesis we know ∀t5:T.(pr3 c t2 t5)→(ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t)
                    assume t5: T
                    suppose H3: pr3 c t3 t5
                      by (pr3_strip . . . H3 . H0)
                      we proved ex2 T λt:T.pr3 c t5 t λt:T.pr3 c t2 t
                      we proceed by induction on the previous result to prove ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t
                         case ex_intro2 : x:T H4:pr3 c t5 x H5:pr3 c t2 x ⇒
                            the thesis becomes ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t
                               by (H2 . H5)
                               we proved ex2 T λt:T.pr3 c t4 t λt:T.pr3 c x t
                               we proceed by induction on the previous result to prove ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t
                                  case ex_intro2 : x0:T H6:pr3 c t4 x0 H7:pr3 c x x0 ⇒
                                     the thesis becomes ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t
                                        by (pr3_t . . . H4 . H7)
                                        we proved pr3 c t5 x0
                                        by (ex_intro2 . . . . H6 previous)
ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t
ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t
                      we proved ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t
∀t5:T.∀H3:(pr3 c t3 t5).(ex2 T λt:T.pr3 c t4 t λt:T.pr3 c t5 t)
          we proved ∀t3:T.(pr3 c t0 t3)→(ex2 T λt4:T.pr3 c t1 t4 λt4:T.pr3 c t3 t4)
       we proved ∀c:C.∀t0:T.∀t1:T.(pr3 c t0 t1)→∀t3:T.(pr3 c t0 t3)→(ex2 T λt4:T.pr3 c t1 t4 λt4:T.pr3 c t3 t4)