DEFINITION nf2_pr3_unfold()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr3 c t1 t2)→(nf2 c t1)→(eq T t1 t2)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr3 c t1 t2
          we proceed by induction on H to prove (nf2 c t1)→(eq T t1 t2)
             case pr3_refl : t:T ⇒
                the thesis becomes ∀H0:(nf2 c t).(eq T t t)
                   suppose H0: nf2 c t
                      by (pr0_refl .)
                      we proved pr0 t t
                      by (pr2_free . . . previous)
                      we proved pr2 c t t
                      by (H0 . previous)
                      we proved eq T t t
∀H0:(nf2 c t).(eq T t t)
             case pr3_sing : t0:T t3:T H0:pr2 c t3 t0 t4:T :pr3 c t0 t4 ⇒
                the thesis becomes ∀H3:(nf2 c t3).(eq T t3 t4)
                (H2) by induction hypothesis we know (nf2 c t0)→(eq T t0 t4)
                   suppose H3: nf2 c t3
                      (H4) consider H3
                      (H5) 
                         by (H4 . H0)
                         we proved eq T t3 t0
                         we proceed by induction on the previous result to prove nf2 c t0
                            case refl_equal : ⇒
                               the thesis becomes the hypothesis H3
nf2 c t0
                      end of H5
                      (h1) by (H2 H5) we proved eq T t0 t4
                      (h2) by (H4 . H0) we proved eq T t3 t0
                      by (eq_ind_r . . . h1 . h2)
                      we proved eq T t3 t4
∀H3:(nf2 c t3).(eq T t3 t4)
          we proved (nf2 c t1)→(eq T t1 t2)
       we proved ∀c:C.∀t1:T.∀t2:T.(pr3 c t1 t2)→(nf2 c t1)→(eq T t1 t2)