DEFINITION sn3_change()
TYPE =
       ∀b:B
         .not (eq B b Abbr)
           →∀c:C.∀v1:T.∀t:T.(sn3 (CHead c (Bind b) v1) t)→∀v2:T.(sn3 (CHead c (Bind b) v2) t)
BODY =
        assume b: B
        suppose H: not (eq B b Abbr)
        assume c: C
        assume v1: T
        assume t: T
        suppose H0: sn3 (CHead c (Bind b) v1) t
        assume v2: T
          we proceed by induction on H0 to prove sn3 (CHead c (Bind b) v2) t
             case sn3_sing : t1:T :∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 (CHead c (Bind b) v1) t1 t2)→(sn3 (CHead c (Bind b) v1) t2) ⇒
                the thesis becomes sn3 (CHead c (Bind b) v2) t1
                (H2) by induction hypothesis we know 
                   ∀t2:T
                     .(eq T t1 t2)→∀P:Prop.P
                       →(pr3 (CHead c (Bind b) v1) t1 t2)→(sn3 (CHead c (Bind b) v2) t2)
                    assume t2: T
                    suppose H3: (eq T t1 t2)→∀P:Prop.P
                    suppose H4: pr2 (CHead c (Bind b) v2) t1 t2
                      by (pr2_change . H . . . . H4 .)
                      we proved pr2 (CHead c (Bind b) v1) t1 t2
                      by (pr3_pr2 . . . previous)
                      we proved pr3 (CHead c (Bind b) v1) t1 t2
                      by (H2 . H3 previous)
                      we proved sn3 (CHead c (Bind b) v2) t2
                   we proved 
                      ∀t2:T
                        .(eq T t1 t2)→∀P:Prop.P
                          →(pr2 (CHead c (Bind b) v2) t1 t2)→(sn3 (CHead c (Bind b) v2) t2)
                   by (sn3_pr2_intro . . previous)
sn3 (CHead c (Bind b) v2) t1
          we proved sn3 (CHead c (Bind b) v2) t
       we proved 
          ∀b:B
            .not (eq B b Abbr)
              →∀c:C.∀v1:T.∀t:T.(sn3 (CHead c (Bind b) v1) t)→∀v2:T.(sn3 (CHead c (Bind b) v2) t)