DEFINITION pr3_gen_bind()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀c:C
                .∀u1:T
                  .∀t1:T
                    .∀x:T
                      .pr3 c (THead (Bind b) u1 t1) x
                        →(or
                             ex3_2
                               T
                               T
                               λu2:T.λt2:T.eq T x (THead (Bind b) u2 t2)
                               λu2:T.λ:T.pr3 c u1 u2
                               λ:T.λt2:T.pr3 (CHead c (Bind b) u1) t1 t2
                             pr3 (CHead c (Bind b) u1) t1 (lift (S O) O x))
BODY =
Show proof