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