DEFINITION sn3_appl_beta()
TYPE =
       ∀c:C
         .∀u:T
           .∀v:T
             .∀t:T
               .sn3 c (THead (Flat Appl) u (THead (Bind Abbr) v t))
                 →∀w:T
                      .sn3 c w
                        →(sn3
                             c
                             THead
                               Flat Appl
                               u
                               THead (Flat Appl) v (THead (Bind Abst) w t))
BODY =
        assume c: C
        assume u: T
        assume v: T
        assume t: T
        suppose H: sn3 c (THead (Flat Appl) u (THead (Bind Abbr) v t))
        assume w: T
        suppose H0: sn3 c w
          (H_x) 
             by (sn3_gen_flat . . . . H)
land (sn3 c u) (sn3 c (THead (Bind Abbr) v t))
          end of H_x
          (H1) consider H_x
          we proceed by induction on H1 to prove 
             sn3
               c
               THead
                 Flat Appl
                 u
                 THead (Flat Appl) v (THead (Bind Abst) w t)
             case conj : H2:sn3 c u H3:sn3 c (THead (Bind Abbr) v t) ⇒
                the thesis becomes 
                sn3
                  c
                  THead
                    Flat Appl
                    u
                    THead (Flat Appl) v (THead (Bind Abst) w t)
                   (h1) 
                      by (sn3_beta . . . H3 . H0)
sn3 c (THead (Flat Appl) v (THead (Bind Abst) w t))
                   end of h1
                   (h2) 
                       assume u2: T
                       suppose H4: pr3 c (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
                       suppose H5: 
                          iso (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
                            →∀P:Prop.P
                         by (pr3_iso_beta . . . . . H4 H5)
                         we proved pr3 c (THead (Bind Abbr) v t) u2
                         by (pr3_thin_dx . . . previous . .)
                         we proved 
                            pr3
                              c
                              THead (Flat Appl) u (THead (Bind Abbr) v t)
                              THead (Flat Appl) u u2
                         by (sn3_pr3_trans . . H . previous)
                         we proved sn3 c (THead (Flat Appl) u u2)

                         ∀u2:T
                           .pr3 c (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
                             →(iso (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
                                    →∀P:Prop.P
                                  →sn3 c (THead (Flat Appl) u u2))
                   end of h2
                   by (sn3_appl_appl . . . h1 . H2 h2)

                      sn3
                        c
                        THead
                          Flat Appl
                          u
                          THead (Flat Appl) v (THead (Bind Abst) w t)
          we proved 
             sn3
               c
               THead
                 Flat Appl
                 u
                 THead (Flat Appl) v (THead (Bind Abst) w t)
       we proved 
          ∀c:C
            .∀u:T
              .∀v:T
                .∀t:T
                  .sn3 c (THead (Flat Appl) u (THead (Bind Abbr) v t))
                    →∀w:T
                         .sn3 c w
                           →(sn3
                                c
                                THead
                                  Flat Appl
                                  u
                                  THead (Flat Appl) v (THead (Bind Abst) w t))