DEFINITION sn3_appl_appls()
TYPE =
       ∀v1:T
         .∀t1:T
           .∀vs:TList
             .let u1 := THeads (Flat Appl) (TCons v1 vs) t1
             in ∀c:C
                    .sn3 c u1
                      →∀v2:T
                           .sn3 c v2
                             →(∀u2:T.(pr3 c u1 u2)→((iso u1 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
                                  →sn3 c (THead (Flat Appl) v2 u1))
BODY =
Show proof