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 =
        assume c: C
        assume P: T→Prop
        suppose H: 
           ∀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)
          (aux) by well-founded reasoning we prove ∀t:T.(sn3 c t)→(P t)
           assume t: T
           suppose H1: sn3 c t
             by cases on H1 we prove P t
                case sn3_sing t1:T H2:∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2) ⇒
                   the thesis becomes P t1
                    assume t2: T
                    suppose H3: (eq T t1 t2)→∀P:Prop.P
                    suppose H4: pr3 c t1 t2
                      by (H2 . H3 H4)
                      we proved sn3 c t2
                      by (aux . previous)
                      we proved P t2
                   we proved ∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(P t2)
                   by (H . H2 previous)
P t1
             we proved P t
∀t:T.(sn3 c t)→(P t)
          done
          consider aux
          we proved ∀t:T.(sn3 c t)→(P t)
       we proved 
          ∀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)