DEFINITION pr2_confluence__pr2_free_delta()
TYPE =
       ∀c:C
         .∀d:C
           .∀t0:T
             .∀t1:T
               .∀t2:T
                 .∀t4:T
                   .∀u:T
                     .∀i:nat
                       .pr0 t0 t1
                         →(getl i c (CHead d (Bind Abbr) u)
                              →(pr0 t0 t4)→(subst0 i u t4 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t))
BODY =
        assume c: C
        assume d: C
        assume t0: T
        assume t1: T
        assume t2: T
        assume t4: T
        assume u: T
        assume i: nat
        suppose H: pr0 t0 t1
        suppose H0: getl i c (CHead d (Bind Abbr) u)
        suppose H1: pr0 t0 t4
        suppose H2: subst0 i u t4 t2
          by (pr0_confluence . . H1 . H)
          we proved ex2 T λt:T.pr0 t4 t λt:T.pr0 t1 t
          we proceed by induction on the previous result to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
             case ex_intro2 : x:T H3:pr0 t4 x H4:pr0 t1 x ⇒
                the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
                   by (pr0_refl .)
                   we proved pr0 u u
                   by (pr0_subst0 . . H3 . . . H2 . previous)
                   we proved or (pr0 t2 x) (ex2 T λw2:T.pr0 t2 w2 λw2:T.subst0 i u x w2)
                   we proceed by induction on the previous result to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
                      case or_introl : H5:pr0 t2 x ⇒
                         the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
                            (h1) 
                               by (pr2_free . . . H4)
pr2 c t1 x
                            end of h1
                            (h2) 
                               by (pr2_free . . . H5)
pr2 c t2 x
                            end of h2
                            by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
                      case or_intror : H5:ex2 T λw2:T.pr0 t2 w2 λw2:T.subst0 i u x w2 ⇒
                         the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
                            we proceed by induction on H5 to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
                               case ex_intro2 : x0:T H6:pr0 t2 x0 H7:subst0 i u x x0 ⇒
                                  the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
                                     (h1) 
                                        by (pr2_delta . . . . H0 . . H4 . H7)
pr2 c t1 x0
                                     end of h1
                                     (h2) 
                                        by (pr2_free . . . H6)
pr2 c t2 x0
                                     end of h2
                                     by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
          we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
       we proved 
          ∀c:C
            .∀d:C
              .∀t0:T
                .∀t1:T
                  .∀t2:T
                    .∀t4:T
                      .∀u:T
                        .∀i:nat
                          .pr0 t0 t1
                            →(getl i c (CHead d (Bind Abbr) u)
                                 →(pr0 t0 t4)→(subst0 i u t4 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t))