DEFINITION pr2_gen_abbr()
TYPE =
       ∀c:C
         .∀u1:T
           .∀t1:T
             .∀x:T
               .pr2 c (THead (Bind Abbr) u1 t1) x
                 →(or
                      ex3_2
                        T
                        T
                        λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
                        λu2:T.λ:T.pr2 c u1 u2
                        λ:T
                          .λt2:T
                            .or3
                              ∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2)
                              ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c (Bind Abbr) u) t1 t2
                              ex3_2
                                T
                                T
                                λy:T.λ:T.pr2 (CHead c (Bind Abbr) u1) t1 y
                                λy:T.λz:T.pr0 y z
                                λ:T.λz:T.pr2 (CHead c (Bind Abbr) u1) z t2
                      ∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x)))
BODY =
Show proof