DEFINITION sn3_appl_appl()
TYPE =
       ∀v1:T
         .∀t1:T
           .let u1 := THead (Flat Appl) v1 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