DEFINITION nf2_sn3()
TYPE =
       ∀c:C.∀t:T.(sn3 c t)→(ex2 T λu:T.pr3 c t u λu:T.nf2 c u)
BODY =
        assume c: C
        assume t: T
        suppose H: sn3 c t
          we proceed by induction on H to prove ex2 T λu:T.pr3 c t u λu:T.nf2 c u
             case sn3_sing : t1:T :∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2) ⇒
                the thesis becomes ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
                (H1) by induction hypothesis we know ∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(ex2 T λu:T.pr3 c t2 u λu:T.nf2 c u)
                   (H_x) 
                      by (nf2_dec . .)
or (nf2 c t1) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c t1 t2)
                   end of H_x
                   (H2) consider H_x
                   we proceed by induction on H2 to prove ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
                      case or_introl : H3:nf2 c t1 ⇒
                         the thesis becomes ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
                            by (pr3_refl . .)
                            we proved pr3 c t1 t1
                            by (ex_intro2 . . . . previous H3)
ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
                      case or_intror : H3:ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c t1 t2 ⇒
                         the thesis becomes ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
                            we proceed by induction on H3 to prove ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
                               case ex_intro2 : x:T H4:(eq T t1 x)→∀P:Prop.P H5:pr2 c t1 x ⇒
                                  the thesis becomes ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
                                     (H_y) 
                                        by (H1 . H4)
(pr3 c t1 x)→(ex2 T λu:T.pr3 c x u λu:T.nf2 c u)
                                     end of H_y
                                     (H6) 
                                        by (pr3_pr2 . . . H5)
                                        we proved pr3 c t1 x
                                        by (H_y previous)
ex2 T λu:T.pr3 c x u λu:T.nf2 c u
                                     end of H6
                                     we proceed by induction on H6 to prove ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
                                        case ex_intro2 : x0:T H7:pr3 c x x0 H8:nf2 c x0 ⇒
                                           the thesis becomes ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
                                              by (pr3_sing . . . H5 . H7)
                                              we proved pr3 c t1 x0
                                              by (ex_intro2 . . . . previous H8)
ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
ex2 T λu:T.pr3 c t1 u λu:T.nf2 c u
          we proved ex2 T λu:T.pr3 c t u λu:T.nf2 c u
       we proved ∀c:C.∀t:T.(sn3 c t)→(ex2 T λu:T.pr3 c t u λu:T.nf2 c u)