DEFINITION pc3_eta()
TYPE =
       ∀c:C
         .∀t:T
           .∀w:T
             .∀u:T
               .pc3 c t (THead (Bind Abst) w u)
                 →∀v:T
                      .pc3 c v w
                        →(pc3
                             c
                             THead
                               Bind Abst
                               v
                               THead (Flat Appl) (TLRef O) (lift (S O) O t)
                             t)
BODY =
        assume c: C
        assume t: T
        assume w: T
        assume u: T
        suppose H: pc3 c t (THead (Bind Abst) w u)
        assume v: T
        suppose H0: pc3 c v w
          (h1) 
             by (drop_refl .)
             we proved drop O O c c
             that is equivalent to drop (r (Bind Abst) O) O c c
             by (drop_drop . . . . previous .)
             we proved drop (S O) O (CHead c (Bind Abst) v) c
             by (pc3_lift . . . . previous . . H)
             we proved 
                pc3
                  CHead c (Bind Abst) v
                  lift (S O) O t
                  lift (S O) O (THead (Bind Abst) w u)
             by (pc3_thin_dx . . . previous . .)
             we proved 
                pc3
                  CHead c (Bind Abst) v
                  THead (Flat Appl) (TLRef O) (lift (S O) O t)
                  THead
                    Flat Appl
                    TLRef O
                    lift (S O) O (THead (Bind Abst) w u)
             by (pc3_head_21 . . . H0 . . . previous)

                pc3
                  c
                  THead
                    Bind Abst
                    v
                    THead (Flat Appl) (TLRef O) (lift (S O) O t)
                  THead
                    Bind Abst
                    w
                    THead
                      Flat Appl
                      TLRef O
                      lift (S O) O (THead (Bind Abst) w u)
          end of h1
          (h2) 
             (h1) 
                by (pr3_refl . .)
                we proved pr3 c w w
                by (pr3_eta . . . . previous)
                we proved 
                   pr3
                     c
                     THead
                       Bind Abst
                       w
                       THead
                         Flat Appl
                         TLRef O
                         lift (S O) O (THead (Bind Abst) w u)
                     THead (Bind Abst) w u
                by (pc3_pr3_r . . . previous)

                   pc3
                     c
                     THead
                       Bind Abst
                       w
                       THead
                         Flat Appl
                         TLRef O
                         lift (S O) O (THead (Bind Abst) w u)
                     THead (Bind Abst) w u
             end of h1
             (h2) 
                by (pc3_s . . . H)
pc3 c (THead (Bind Abst) w u) t
             end of h2
             by (pc3_t . . . h1 . h2)

                pc3
                  c
                  THead
                    Bind Abst
                    w
                    THead
                      Flat Appl
                      TLRef O
                      lift (S O) O (THead (Bind Abst) w u)
                  t
          end of h2
          by (pc3_t . . . h1 . h2)
          we proved 
             pc3
               c
               THead
                 Bind Abst
                 v
                 THead (Flat Appl) (TLRef O) (lift (S O) O t)
               t
       we proved 
          ∀c:C
            .∀t:T
              .∀w:T
                .∀u:T
                  .pc3 c t (THead (Bind Abst) w u)
                    →∀v:T
                         .pc3 c v w
                           →(pc3
                                c
                                THead
                                  Bind Abst
                                  v
                                  THead (Flat Appl) (TLRef O) (lift (S O) O t)
                                t)