DEFINITION pr2_delta1()
TYPE =
       ∀c:C
         .∀d:C
           .∀u:T
             .∀i:nat
               .getl i c (CHead d (Bind Abbr) u)
                 →∀t1:T.∀t2:T.(pr0 t1 t2)→∀t:T.(subst1 i u t2 t)→(pr2 c t1 t)
BODY =
        assume c: C
        assume d: C
        assume u: T
        assume i: nat
        suppose H: getl i c (CHead d (Bind Abbr) u)
        assume t1: T
        assume t2: T
        suppose H0: pr0 t1 t2
        assume t: T
        suppose H1: subst1 i u t2 t
          we proceed by induction on H1 to prove pr2 c t1 t
             case subst1_refl : ⇒
                the thesis becomes pr2 c t1 t2
                   by (pr2_free . . . H0)
pr2 c t1 t2
             case subst1_single : t0:T H2:subst0 i u t2 t0 ⇒
                the thesis becomes pr2 c t1 t0
                   by (pr2_delta . . . . H . . H0 . H2)
pr2 c t1 t0
          we proved pr2 c t1 t
       we proved 
          ∀c:C
            .∀d:C
              .∀u:T
                .∀i:nat
                  .getl i c (CHead d (Bind Abbr) u)
                    →∀t1:T.∀t2:T.(pr0 t1 t2)→∀t:T.(subst1 i u t2 t)→(pr2 c t1 t)