DEFINITION pr0_gen_abst()
TYPE =
       ∀u1:T
         .∀t1:T
           .∀x:T
             .pr0 (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.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
BODY =
Show proof