DEFINITION pr3_iso_appls_cast()
TYPE =
       ∀c:C
         .∀v:T
           .∀t:T
             .∀vs:TList
               .let u1 := THeads (Flat Appl) vs (THead (Flat Cast) v t)
               in ∀u2:T
                      .pr3 c u1 u2
                        →((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) vs t) u2)
BODY =
Show proof