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 =
        assume v1: T
        assume t1: T
        assume vs: TList
          we must prove 
                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))
          or equivalently 
                ∀c:C
                  .sn3 c (THeads (Flat Appl) (TCons v1 vs) t1)
                    →∀v2:T
                         .sn3 c v2
                           →(∀u2:T
                                  .pr3 c (THeads (Flat Appl) (TCons v1 vs) t1) u2
                                    →((iso (THeads (Flat Appl) (TCons v1 vs) t1) u2)→∀P:Prop.P
                                         →sn3 c (THead (Flat Appl) v2 u2))
                                →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1)))
          assume c: C
             we must prove 
                   sn3 c (THeads (Flat Appl) (TCons v1 vs) t1)
                     →∀v2:T
                          .sn3 c v2
                            →(∀u2:T
                                   .pr3 c (THeads (Flat Appl) (TCons v1 vs) t1) u2
                                     →((iso (THeads (Flat Appl) (TCons v1 vs) t1) u2)→∀P:Prop.P
                                          →sn3 c (THead (Flat Appl) v2 u2))
                                 →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1)))
             or equivalently 
                   sn3 c (THead (Flat Appl) v1 (THeads (Flat Appl) vs t1))
                     →∀v2:T
                          .sn3 c v2
                            →(∀u2:T
                                   .pr3 c (THeads (Flat Appl) (TCons v1 vs) t1) u2
                                     →((iso (THeads (Flat Appl) (TCons v1 vs) t1) u2)→∀P:Prop.P
                                          →sn3 c (THead (Flat Appl) v2 u2))
                                 →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1)))
              suppose H: sn3 c (THead (Flat Appl) v1 (THeads (Flat Appl) vs t1))
              assume v2: T
              suppose H0: sn3 c v2
                we must prove 
                      ∀u2:T
                          .pr3 c (THeads (Flat Appl) (TCons v1 vs) t1) u2
                            →((iso (THeads (Flat Appl) (TCons v1 vs) t1) u2)→∀P:Prop.P
                                 →sn3 c (THead (Flat Appl) v2 u2))
                        →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1))
                or equivalently 
                      ∀u2:T
                          .pr3 c (THead (Flat Appl) v1 (THeads (Flat Appl) vs t1)) u2
                            →(iso (THead (Flat Appl) v1 (THeads (Flat Appl) vs t1)) u2
                                   →∀P:Prop.P
                                 →sn3 c (THead (Flat Appl) v2 u2))
                        →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1))
                suppose H1: 
                   ∀u2:T
                     .pr3 c (THead (Flat Appl) v1 (THeads (Flat Appl) vs t1)) u2
                       →(iso (THead (Flat Appl) v1 (THeads (Flat Appl) vs t1)) u2
                              →∀P:Prop.P
                            →sn3 c (THead (Flat Appl) v2 u2))
                   by (sn3_appl_appl . . . H . H0 H1)
                   we proved 
                      sn3
                        c
                        THead
                          Flat Appl
                          v2
                          THead (Flat Appl) v1 (THeads (Flat Appl) vs t1)
                   that is equivalent to sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1))
                we proved 
                   ∀u2:T
                       .pr3 c (THead (Flat Appl) v1 (THeads (Flat Appl) vs t1)) u2
                         →(iso (THead (Flat Appl) v1 (THeads (Flat Appl) vs t1)) u2
                                →∀P:Prop.P
                              →sn3 c (THead (Flat Appl) v2 u2))
                     →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1))
                that is equivalent to 
                   ∀u2:T
                       .pr3 c (THeads (Flat Appl) (TCons v1 vs) t1) u2
                         →((iso (THeads (Flat Appl) (TCons v1 vs) t1) u2)→∀P:Prop.P
                              →sn3 c (THead (Flat Appl) v2 u2))
                     →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1))
             we proved 
                sn3 c (THead (Flat Appl) v1 (THeads (Flat Appl) vs t1))
                  →∀v2:T
                       .sn3 c v2
                         →(∀u2:T
                                .pr3 c (THeads (Flat Appl) (TCons v1 vs) t1) u2
                                  →((iso (THeads (Flat Appl) (TCons v1 vs) t1) u2)→∀P:Prop.P
                                       →sn3 c (THead (Flat Appl) v2 u2))
                              →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1)))
             that is equivalent to 
                sn3 c (THeads (Flat Appl) (TCons v1 vs) t1)
                  →∀v2:T
                       .sn3 c v2
                         →(∀u2:T
                                .pr3 c (THeads (Flat Appl) (TCons v1 vs) t1) u2
                                  →((iso (THeads (Flat Appl) (TCons v1 vs) t1) u2)→∀P:Prop.P
                                       →sn3 c (THead (Flat Appl) v2 u2))
                              →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1)))
          we proved 
             ∀c:C
               .sn3 c (THeads (Flat Appl) (TCons v1 vs) t1)
                 →∀v2:T
                      .sn3 c v2
                        →(∀u2:T
                               .pr3 c (THeads (Flat Appl) (TCons v1 vs) t1) u2
                                 →((iso (THeads (Flat Appl) (TCons v1 vs) t1) u2)→∀P:Prop.P
                                      →sn3 c (THead (Flat Appl) v2 u2))
                             →sn3 c (THead (Flat Appl) v2 (THeads (Flat Appl) (TCons v1 vs) t1)))
          that is equivalent to 
             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))
       we proved 
          ∀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))