DEFINITION sn3_pr3_trans()
TYPE =
       ∀c:C.∀t1:T.(sn3 c t1)→∀t2:T.(pr3 c t1 t2)→(sn3 c t2)
BODY =
        assume c: C
        assume t1: T
        suppose H: sn3 c t1
          we proceed by induction on H to prove ∀t2:T.(pr3 c t1 t2)→(sn3 c t2)
             case sn3_sing : t2:T H0:∀t3:T.((eq T t2 t3)→∀P:Prop.P)→(pr3 c t2 t3)→(sn3 c t3) ⇒
                the thesis becomes ∀t3:T.∀H2:(pr3 c t2 t3).(sn3 c t3)
                (H1) by induction hypothesis we know ∀t3:T.((eq T t2 t3)→∀P:Prop.P)→(pr3 c t2 t3)→∀t4:T.(pr3 c t3 t4)→(sn3 c t4)
                    assume t3: T
                    suppose H2: pr3 c t2 t3
                       assume t0: T
                       suppose H3: (eq T t3 t0)→∀P:Prop.P
                       suppose H4: pr3 c t3 t0
                         (H_x) 
                            by (term_dec . .)
or (eq T t2 t3) (eq T t2 t3)→∀P:Prop.P
                         end of H_x
                         (H5) consider H_x
                         we proceed by induction on H5 to prove sn3 c t0
                            case or_introl : H6:eq T t2 t3 ⇒
                               the thesis becomes sn3 c t0
                                  (H7) 
                                     by (eq_ind_r . . . H4 . H6)
pr3 c t2 t0
                                  end of H7
                                  (H8) 
                                     by (eq_ind_r . . . H3 . H6)
(eq T t2 t0)→∀P:Prop.P
                                  end of H8
                                  by (H0 . H8 H7)
sn3 c t0
                            case or_intror : H6:(eq T t2 t3)→∀P:Prop.P ⇒
                               the thesis becomes sn3 c t0
                                  by (H1 . H6 H2 . H4)
sn3 c t0
                         we proved sn3 c t0
                      we proved ∀t0:T.((eq T t3 t0)→∀P:Prop.P)→(pr3 c t3 t0)→(sn3 c t0)
                      by (sn3_sing . . previous)
                      we proved sn3 c t3
∀t3:T.∀H2:(pr3 c t2 t3).(sn3 c t3)
          we proved ∀t2:T.(pr3 c t1 t2)→(sn3 c t2)
       we proved ∀c:C.∀t1:T.(sn3 c t1)→∀t2:T.(pr3 c t1 t2)→(sn3 c t2)