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