DEFINITION pr0_confluence__pr0_delta_tau()
TYPE =
       ∀u2:T
         .∀t3:T
           .∀w:T
             .subst0 O u2 t3 w
               →∀t4:T
                    .pr0 (lift (S O) O t4) t3
                      →∀t2:T.(ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 t2 t)
BODY =
        assume u2: T
        assume t3: T
        assume w: T
        suppose H: subst0 O u2 t3 w
        assume t4: T
        suppose H0: pr0 (lift (S O) O t4) t3
        assume t2: T
          by (pr0_gen_lift . . . . H0)
          we proved ex2 T λt2:T.eq T t3 (lift (S O) O t2) λt2:T.pr0 t4 t2
          we proceed by induction on the previous result to prove ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 t2 t
             case ex_intro2 : x:T H1:eq T t3 (lift (S O) O x) :pr0 t4 x ⇒
                the thesis becomes ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 t2 t
                   (H3) 
                      we proceed by induction on H1 to prove subst0 O u2 (lift (S O) O x) w
                         case refl_equal : ⇒
                            the thesis becomes the hypothesis H
subst0 O u2 (lift (S O) O x) w
                   end of H3
                   (h1) by (le_n .) we proved le O O
                   (h2) 
                      (h1) 
                         by (le_n .)
                         we proved le (plus (S O) O) (plus (S O) O)
lt O (plus (S O) O)
                      end of h1
                      (h2) 
                         by (plus_sym . .)
eq nat (plus O (S O)) (plus (S O) O)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
lt O (plus O (S O))
                   end of h2
                   by (subst0_gen_lift_false . . . . . . h1 h2 H3 .)
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 t2 t
          we proved ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 t2 t
       we proved 
          ∀u2:T
            .∀t3:T
              .∀w:T
                .subst0 O u2 t3 w
                  →∀t4:T
                       .pr0 (lift (S O) O t4) t3
                         →∀t2:T.(ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 t2 t)