DEFINITION pr2_gen_abst()
TYPE =
       ∀c:C
         .∀u1:T
           .∀t1:T
             .∀x:T
               .pr2 c (THead (Bind Abst) u1 t1) x
                 →(ex3_2
                      T
                      T
                      λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
                      λu2:T.λ:T.pr2 c u1 u2
                      λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2))
BODY =
Show proof