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 =
Show proof