DEFINITION pr2_confluence__pr2_free_free()
TYPE =
       ∀c:C.∀t0:T.∀t1:T.∀t2:T.(pr0 t0 t1)→(pr0 t0 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
BODY =
        assume c: C
        assume t0: T
        assume t1: T
        assume t2: T
        suppose H: pr0 t0 t1
        suppose H0: pr0 t0 t2
          by (pr0_confluence . . H0 . H)
          we proved ex2 T λt:T.pr0 t2 t λt:T.pr0 t1 t
          we proceed by induction on the previous result to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
             case ex_intro2 : x:T H1:pr0 t2 x H2:pr0 t1 x ⇒
                the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
                   (h1) 
                      by (pr2_free . . . H2)
pr2 c t1 x
                   end of h1
                   (h2) 
                      by (pr2_free . . . H1)
pr2 c t2 x
                   end of h2
                   by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
          we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
       we proved ∀c:C.∀t0:T.∀t1:T.∀t2:T.(pr0 t0 t1)→(pr0 t0 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)