DEFINITION sn3_cpr3_trans()
TYPE =
       ∀c:C.∀u1:T.∀u2:T.(pr3 c u1 u2)→∀k:K.∀t:T.(sn3 (CHead c k u1) t)→(sn3 (CHead c k u2) t)
BODY =
        assume c: C
        assume u1: T
        assume u2: T
        suppose H: pr3 c u1 u2
        assume k: K
        assume t: T
        suppose H0: sn3 (CHead c k u1) t
          we proceed by induction on H0 to prove sn3 (CHead c k u2) t
             case sn3_sing : t1:T :∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 (CHead c k u1) t1 t2)→(sn3 (CHead c k u1) t2) ⇒
                the thesis becomes sn3 (CHead c k u2) t1
                (H2) by induction hypothesis we know ∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 (CHead c k u1) t1 t2)→(sn3 (CHead c k u2) t2)
                    assume t2: T
                    suppose H3: (eq T t1 t2)→∀P:Prop.P
                    suppose H4: pr3 (CHead c k u2) t1 t2
                      by (pr3_pr3_pr3_t . . . H . . . H4)
                      we proved pr3 (CHead c k u1) t1 t2
                      by (H2 . H3 previous)
                      we proved sn3 (CHead c k u2) t2
                   we proved ∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 (CHead c k u2) t1 t2)→(sn3 (CHead c k u2) t2)
                   by (sn3_sing . . previous)
sn3 (CHead c k u2) t1
          we proved sn3 (CHead c k u2) t
       we proved ∀c:C.∀u1:T.∀u2:T.(pr3 c u1 u2)→∀k:K.∀t:T.(sn3 (CHead c k u1) t)→(sn3 (CHead c k u2) t)