DEFINITION nf2_pr3_confluence()
TYPE =
       ∀c:C.∀t1:T.(nf2 c t1)→∀t2:T.(nf2 c t2)→∀t:T.(pr3 c t t1)→(pr3 c t t2)→(eq T t1 t2)
BODY =
        assume c: C
        assume t1: T
        suppose H: nf2 c t1
        assume t2: T
        suppose H0: nf2 c t2
        assume t: T
        suppose H1: pr3 c t t1
        suppose H2: pr3 c t t2
          by (pr3_confluence . . . H2 . H1)
          we proved ex2 T λt:T.pr3 c t2 t λt:T.pr3 c t1 t
          we proceed by induction on the previous result to prove eq T t1 t2
             case ex_intro2 : x:T H3:pr3 c t2 x H4:pr3 c t1 x ⇒
                the thesis becomes eq T t1 t2
                   (H_y) 
                      by (nf2_pr3_unfold . . . H4 H)
eq T t1 x
                   end of H_y
                   (H6) 
                      by (eq_ind_r . . . H3 . H_y)
pr3 c t2 t1
                   end of H6
                   (H_y0) 
                      by (nf2_pr3_unfold . . . H6 H0)
eq T t2 t1
                   end of H_y0
                   by (refl_equal . .)
                   we proved eq T t1 t1
                   by (eq_ind_r . . . previous . H_y0)
eq T t1 t2
          we proved eq T t1 t2
       we proved ∀c:C.∀t1:T.(nf2 c t1)→∀t2:T.(nf2 c t2)→∀t:T.(pr3 c t t1)→(pr3 c t t2)→(eq T t1 t2)