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