DEFINITION sn3_pr2_intro()
TYPE =
       ∀c:C.∀t1:T.(∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr2 c t1 t2)→(sn3 c t2))→(sn3 c t1)
BODY =
        assume c: C
        assume t1: T
        suppose H: ∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr2 c t1 t2)→(sn3 c t2)
           assume t2: T
           suppose H0: (eq T t1 t2)→∀P:Prop.P
           suppose H1: pr3 c t1 t2
             (H2) consider H0
             (H3) consider H
                assume t: T
                 suppose H4: ∀t3:T.((eq T t t3)→∀P:Prop.P)→(pr2 c t t3)→(sn3 c t3)
                 suppose H5: (eq T t t)→∀P:Prop.P
                   by (pr0_refl .)
                   we proved pr0 t t
                   by (pr2_free . . . previous)
                   we proved pr2 c t t
                   by (H4 . H5 previous)
                   we proved sn3 c t

                   ∀H4:∀t3:T.((eq T t t3)→∀P:Prop.P)→(pr2 c t t3)→(sn3 c t3)
                     .∀H5:(eq T t t)→∀P:Prop.P.(sn3 c t)
              assume t3: T
              assume t4: T
              suppose H4: pr2 c t4 t3
              assume t5: T
              suppose H5: pr3 c t3 t5
                 suppose H6: 
                    ∀t6:T.((eq T t3 t6)→∀P:Prop.P)→(pr2 c t3 t6)→(sn3 c t6)
                      →((eq T t3 t5)→∀P:Prop.P)→(sn3 c t5)
                 suppose H7: ∀t6:T.((eq T t4 t6)→∀P:Prop.P)→(pr2 c t4 t6)→(sn3 c t6)
                 suppose H8: (eq T t4 t5)→∀P:Prop.P
                   (H_x) 
                      by (term_dec . .)
or (eq T t4 t3) (eq T t4 t3)→∀P:Prop.P
                   end of H_x
                   (H9) consider H_x
                   we proceed by induction on H9 to prove sn3 c t5
                      case or_introl : H10:eq T t4 t3 ⇒
                         the thesis becomes sn3 c t5
                            (H11) 
                               we proceed by induction on H10 to prove (eq T t3 t5)→∀P:Prop.P
                                  case refl_equal : ⇒
                                     the thesis becomes the hypothesis H8
(eq T t3 t5)→∀P:Prop.P
                            end of H11
                            (H12) 
                               we proceed by induction on H10 to prove ∀t6:T.((eq T t3 t6)→∀P:Prop.P)→(pr2 c t3 t6)→(sn3 c t6)
                                  case refl_equal : ⇒
                                     the thesis becomes the hypothesis H7
∀t6:T.((eq T t3 t6)→∀P:Prop.P)→(pr2 c t3 t6)→(sn3 c t6)
                            end of H12
                            by (H6 H12 H11)
sn3 c t5
                      case or_intror : H10:(eq T t4 t3)→∀P:Prop.P ⇒
                         the thesis becomes sn3 c t5
                            by (H7 . H10 H4)
                            we proved sn3 c t3
                            by (sn3_pr3_trans . . previous . H5)
sn3 c t5
                   we proved sn3 c t5

                   ∀H7:∀t6:T.((eq T t4 t6)→∀P:Prop.P)→(pr2 c t4 t6)→(sn3 c t6)
                     .∀H8:(eq T t4 t5)→∀P:Prop.P.(sn3 c t5)
             by (previous H1 H3)
             we proved ((eq T t1 t2)→∀P:Prop.P)→(sn3 c t2)
             by (previous H2)
             we proved sn3 c t2
          we proved ∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2)
          by (sn3_sing . . previous)
          we proved sn3 c t1
       we proved ∀c:C.∀t1:T.(∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr2 c t1 t2)→(sn3 c t2))→(sn3 c t1)