DEFINITION pr1_eta()
TYPE =
       ∀w:T
         .∀u:T
           .let t := THead (Bind Abst) w u
           in ∀v:T
                  .pr1 v w
                    →(pr1
                         THead
                           Bind Abst
                           v
                           THead (Flat Appl) (TLRef O) (lift (S O) O t)
                         t)
BODY =
        assume w: T
        assume u: T
          we must prove 
                let t := THead (Bind Abst) w u
                in ∀v:T
                       .pr1 v w
                         →(pr1
                              THead
                                Bind Abst
                                v
                                THead (Flat Appl) (TLRef O) (lift (S O) O t)
                              t)
          or equivalently 
                ∀v:T
                  .pr1 v w
                    →(pr1
                         THead
                           Bind Abst
                           v
                           THead
                             Flat Appl
                             TLRef O
                             lift (S O) O (THead (Bind Abst) w u)
                         THead (Bind Abst) w u)
           assume v: T
           suppose H: pr1 v w
             (h1) 
                (h1) 
                   (h1) 
                      by (pr0_refl .)
pr0 (TLRef O) (TLRef O)
                   end of h1
                   (h2) 
                      by (pr0_refl .)
pr0 (lift (S O) (S O) u) (lift (S O) (S O) u)
                   end of h2
                   by (pr0_beta . . . h1 . . h2)

                      pr0
                        THead
                          Flat Appl
                          TLRef O
                          THead (Bind Abst) (lift (S O) O w) (lift (S O) (S O) u)
                        THead (Bind Abbr) (TLRef O) (lift (S O) (S O) u)
                end of h1
                (h2) 
                   (h1) 
                      (h1) 
                         by (pr0_refl .)
pr0 (TLRef O) (TLRef O)
                      end of h1
                      (h2) 
                         by (pr0_refl .)
pr0 (lift (S O) (S O) u) (lift (S O) (S O) u)
                      end of h2
                      (h3) 
                         by (le_n .)
                         we proved le O O
                         by (subst1_lift_S . . . previous)
subst1 O (TLRef O) (lift (S O) (S O) u) (lift (S O) O u)
                      end of h3
                      by (pr0_delta1 . . h1 . . h2 . h3)

                         pr0
                           THead (Bind Abbr) (TLRef O) (lift (S O) (S O) u)
                           THead (Bind Abbr) (TLRef O) (lift (S O) O u)
                   end of h1
                   (h2) 
                      by (pr0_refl .)
                      we proved pr0 u u
                      by (pr0_zeta . not_abbr_abst . . previous .)
                      we proved pr0 (THead (Bind Abbr) (TLRef O) (lift (S O) O u)) u
                      by (pr1_pr0 . . previous)
pr1 (THead (Bind Abbr) (TLRef O) (lift (S O) O u)) u
                   end of h2
                   by (pr1_sing . . h1 . h2)
pr1 (THead (Bind Abbr) (TLRef O) (lift (S O) (S O) u)) u
                end of h2
                by (pr1_sing . . h1 . h2)
                we proved 
                   pr1
                     THead
                       Flat Appl
                       TLRef O
                       THead (Bind Abst) (lift (S O) O w) (lift (S O) (S O) u)
                     u
                by (pr1_comp . . H . . previous .)

                   pr1
                     THead
                       Bind Abst
                       v
                       THead
                         Flat Appl
                         TLRef O
                         THead (Bind Abst) (lift (S O) O w) (lift (S O) (S O) u)
                     THead (Bind Abst) w u
             end of h1
             (h2) 
                by (lift_bind . . . . .)

                   eq
                     T
                     lift (S O) O (THead (Bind Abst) w u)
                     THead (Bind Abst) (lift (S O) O w) (lift (S O) (S O) u)
             end of h2
             by (eq_ind_r . . . h1 . h2)
             we proved 
                pr1
                  THead
                    Bind Abst
                    v
                    THead
                      Flat Appl
                      TLRef O
                      lift (S O) O (THead (Bind Abst) w u)
                  THead (Bind Abst) w u
          we proved 
             ∀v:T
               .pr1 v w
                 →(pr1
                      THead
                        Bind Abst
                        v
                        THead
                          Flat Appl
                          TLRef O
                          lift (S O) O (THead (Bind Abst) w u)
                      THead (Bind Abst) w u)
          that is equivalent to 
             let t := THead (Bind Abst) w u
             in ∀v:T
                    .pr1 v w
                      →(pr1
                           THead
                             Bind Abst
                             v
                             THead (Flat Appl) (TLRef O) (lift (S O) O t)
                           t)
       we proved 
          ∀w:T
            .∀u:T
              .let t := THead (Bind Abst) w u
              in ∀v:T
                     .pr1 v w
                       →(pr1
                            THead
                              Bind Abst
                              v
                              THead (Flat Appl) (TLRef O) (lift (S O) O t)
                            t)