DEFINITION pr3_iso_appls_appl_bind()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀v:T
                .∀u:T
                  .∀t:T
                    .∀vs:TList
                      .let u1 := THeads
                                      Flat Appl
                                      vs
                                      THead (Flat Appl) v (THead (Bind b) u t)
                      in ∀c:C
                             .∀u2:T
                               .pr3 c u1 u2
                                 →((iso u1 u2)→∀P:Prop.P
                                      →(pr3
                                           c
                                           THeads
                                             Flat Appl
                                             vs
                                             THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
                                           u2))
BODY =
Show proof