DEFINITION pr2_ind()
TYPE =
       ∀P:C→T→T→Prop
         .∀c:C.∀t:T.∀t1:T.(pr0 t t1)→(P c t t1)
           →(∀c:C
                  .∀c1:C
                    .∀t:T
                      .∀n:nat
                        .getl n c (CHead c1 (Bind Abbr) t)
                          →∀t1:T.∀t2:T.(pr0 t1 t2)→∀t3:T.(subst0 n t t2 t3)→(P c t1 t3)
                →∀c:C.∀t:T.∀t1:T.(pr2 c t t1)→(P c t t1))
BODY =
        assume P: C→T→T→Prop
        suppose H: ∀c:C.∀t:T.∀t1:T.(pr0 t t1)→(P c t t1)
        suppose H1: 
           ∀c:C
             .∀c1:C
               .∀t:T
                 .∀n:nat
                   .getl n c (CHead c1 (Bind Abbr) t)
                     →∀t1:T.∀t2:T.(pr0 t1 t2)→∀t3:T.(subst0 n t t2 t3)→(P c t1 t3)
        assume c: C
        assume t: T
        assume t1: T
        suppose H2: pr2 c t t1
          by cases on H2 we prove P c t t1
             case pr2_free c1:C t2:T t3:T H3:pr0 t2 t3 ⇒
                the thesis becomes P c1 t2 t3
                by (H . . . H3)
P c1 t2 t3
             case pr2_delta c1:C c2:C t2:T n:nat H3:getl n c1 (CHead c2 (Bind Abbr) t2) t3:T t4:T H4:pr0 t3 t4 t5:T H5:subst0 n t2 t4 t5 ⇒
                the thesis becomes P c1 t3 t5
                by (H1 . . . . H3 . . H4 . H5)
P c1 t3 t5
          we proved P c t t1
       we proved 
          ∀P:C→T→T→Prop
            .∀c:C.∀t:T.∀t1:T.(pr0 t t1)→(P c t t1)
              →(∀c:C
                     .∀c1:C
                       .∀t:T
                         .∀n:nat
                           .getl n c (CHead c1 (Bind Abbr) t)
                             →∀t1:T.∀t2:T.(pr0 t1 t2)→∀t3:T.(subst0 n t t2 t3)→(P c t1 t3)
                   →∀c:C.∀t:T.∀t1:T.(pr2 c t t1)→(P c t t1))