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