DEFINITION pr0_delta1()
TYPE =
       ∀u1:T
         .∀u2:T
           .pr0 u1 u2
             →∀t1:T
                  .∀t2:T
                    .pr0 t1 t2
                      →∀w:T.(subst1 O u2 t2 w)→(pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 w))
BODY =
        assume u1: T
        assume u2: T
        suppose H: pr0 u1 u2
        assume t1: T
        assume t2: T
        suppose H0: pr0 t1 t2
        assume w: T
        suppose H1: subst1 O u2 t2 w
          we proceed by induction on H1 to prove pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 w)
             case subst1_refl : ⇒
                the thesis becomes pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 t2)
                   by (pr0_comp . . H . . H0 .)
pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 t2)
             case subst1_single : t0:T H2:subst0 O u2 t2 t0 ⇒
                the thesis becomes pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 t0)
                   by (pr0_delta . . H . . H0 . H2)
pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 t0)
          we proved pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 w)
       we proved 
          ∀u1:T
            .∀u2:T
              .pr0 u1 u2
                →∀t1:T
                     .∀t2:T
                       .pr0 t1 t2
                         →∀w:T.(subst1 O u2 t2 w)→(pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 w))