DEFINITION pr3_iso_appls_beta()
TYPE =
       ∀us:TList
         .∀v:T
           .∀w:T
             .∀t:T
               .let u1 := THeads
                               Flat Appl
                               us
                               THead (Flat Appl) v (THead (Bind Abst) w t)
               in ∀c:C
                      .∀u2:T
                        .pr3 c u1 u2
                          →((iso u1 u2)→∀P:Prop.P
                               →pr3 c (THeads (Flat Appl) us (THead (Bind Abbr) v t)) u2)
BODY =
Show proof