DEFINITION sc3_appl()
TYPE =
       ∀g:G
         .∀a1:A
           .∀a2:A
             .∀vs:TList
               .∀c:C
                 .∀v:T
                   .∀t:T
                     .sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
                       →(sc3 g a1 c v
                            →∀w:T
                                 .sc3 g (asucc g a1) c w
                                   →(sc3
                                        g
                                        a2
                                        c
                                        THeads
                                          Flat Appl
                                          vs
                                          THead (Flat Appl) v (THead (Bind Abst) w t)))
BODY =
Show proof