DEFINITION pr1_ind()
TYPE =
       ∀P:T→T→Prop
         .∀t:T.(P t t)
           →(∀t:T.∀t1:T.(pr0 t1 t)→∀t2:T.(pr1 t t2)→(P t t2)→(P t1 t2)
                →∀t:T.∀t1:T.(pr1 t t1)→(P t t1))
BODY =
Show proof