DEFINITION pr0_gen_abbr()
TYPE =
       ∀u1:T
         .∀t1:T
           .∀x:T
             .pr0 (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.pr0 u1 u2
                      λu2:T.λt2:T.or (pr0 t1 t2) (ex2 T λy:T.pr0 t1 y λy:T.subst0 O u2 y t2)
                    pr0 t1 (lift (S O) O x))
BODY =
Show proof