DEFINITION pr3_iso_appls_abbr()
TYPE =
       ∀c:C
         .∀d:C
           .∀w:T
             .∀i:nat
               .getl i c (CHead d (Bind Abbr) w)
                 →∀vs:TList
                      .let u1 := THeads (Flat Appl) vs (TLRef i)
                      in ∀u2:T
                             .pr3 c u1 u2
                               →((iso u1 u2)→∀P:Prop.P
                                    →pr3 c (THeads (Flat Appl) vs (lift (S i) O w)) u2)
BODY =
Show proof