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 =
Show proof