DEFINITION sn3_nf2()
TYPE =
       ∀c:C.∀t:T.(nf2 c t)→(sn3 c t)
BODY =
        assume c: C
        assume t: T
        suppose H: nf2 c t
           assume t2: T
           suppose H0: (eq T t t2)→∀P:Prop.P
           suppose H1: pr3 c t t2
             (H_y) 
                by (nf2_pr3_unfold . . . H1 H)
eq T t t2
             end of H_y
             (H3) 
                by (eq_ind_r . . . H0 . H_y)
(eq T t t)→∀P:Prop.P
             end of H3
             we proceed by induction on H_y to prove sn3 c t2
                case refl_equal : ⇒
                   the thesis becomes sn3 c t
                      by (refl_equal . .)
                      we proved eq T t t
                      by (H3 previous .)
sn3 c t
             we proved sn3 c t2
          we proved ∀t2:T.((eq T t t2)→∀P:Prop.P)→(pr3 c t t2)→(sn3 c t2)
          by (sn3_sing . . previous)
          we proved sn3 c t
       we proved ∀c:C.∀t:T.(nf2 c t)→(sn3 c t)