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