DEFINITION pr3_subst1()
TYPE =
       ∀c:C
         .∀e:C
           .∀v:T
             .∀i:nat
               .getl i c (CHead e (Bind Abbr) v)
                 →∀t1:T.∀t2:T.(pr3 c t1 t2)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t2 w2)
BODY =
        assume c: C
        assume e: C
        assume v: T
        assume i: nat
        suppose H: getl i c (CHead e (Bind Abbr) v)
        assume t1: T
        assume t2: T
        suppose H0: pr3 c t1 t2
          we proceed by induction on H0 to prove ∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t2 w2)
             case pr3_refl : t:T ⇒
                the thesis becomes ∀w1:T.∀H1:(subst1 i v t w1).(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t w2)
                    assume w1: T
                    suppose H1: subst1 i v t w1
                      by (pr3_refl . .)
                      we proved pr3 c w1 w1
                      by (ex_intro2 . . . . previous H1)
                      we proved ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t w2
∀w1:T.∀H1:(subst1 i v t w1).(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t w2)
             case pr3_sing : t3:T t4:T H1:pr2 c t4 t3 t5:T :pr3 c t3 t5 ⇒
                the thesis becomes ∀w1:T.∀H4:(subst1 i v t4 w1).(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2)
                (H3) by induction hypothesis we know ∀w1:T.(subst1 i v t3 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2)
                    assume w1: T
                    suppose H4: subst1 i v t4 w1
                      by (pr2_subst1 . . . . H . . H1 . H4)
                      we proved ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t3 w2
                      we proceed by induction on the previous result to prove ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
                         case ex_intro2 : x:T H5:pr2 c w1 x H6:subst1 i v t3 x ⇒
                            the thesis becomes ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
                               by (H3 . H6)
                               we proved ex2 T λw2:T.pr3 c x w2 λw2:T.subst1 i v t5 w2
                               we proceed by induction on the previous result to prove ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
                                  case ex_intro2 : x0:T H7:pr3 c x x0 H8:subst1 i v t5 x0 ⇒
                                     the thesis becomes ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
                                        by (pr3_sing . . . H5 . H7)
                                        we proved pr3 c w1 x0
                                        by (ex_intro2 . . . . previous H8)
ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
                      we proved ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
∀w1:T.∀H4:(subst1 i v t4 w1).(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2)
          we proved ∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t2 w2)
       we proved 
          ∀c:C
            .∀e:C
              .∀v:T
                .∀i:nat
                  .getl i c (CHead e (Bind Abbr) v)
                    →∀t1:T.∀t2:T.(pr3 c t1 t2)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t2 w2)