DEFINITION pr3_eta()
TYPE =
       ∀c:C
         .∀w:T
           .∀u:T
             .let t := THead (Bind Abst) w u
             in ∀v:T
                    .pr3 c v w
                      →(pr3
                           c
                           THead
                             Bind Abst
                             v
                             THead (Flat Appl) (TLRef O) (lift (S O) O t)
                           t)
BODY =
Show proof