DEFINITION sc3_bind()
TYPE =
       ∀g:G
         .∀b:B
           .not (eq B b Abst)
             →∀a1:A
                  .∀a2:A
                    .∀vs:TList
                      .∀c:C
                        .∀v:T
                          .∀t:T
                            .(sc3
                                g
                                a2
                                CHead c (Bind b) v
                                THeads (Flat Appl) (lifts (S O) O vs) t)
                              →(sc3 g a1 c v
                                   →sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind b) v t)))
BODY =
Show proof