DEFINITION pr3_ind()
TYPE =
       ∀c:C
         .∀P:T→T→Prop
           .∀t:T.(P t t)
             →(∀t:T.∀t1:T.(pr2 c t1 t)→∀t2:T.(pr3 c t t2)→(P t t2)→(P t1 t2)
                  →∀t:T.∀t1:T.(pr3 c t t1)→(P t t1))
BODY =
Show proof