DEFINITION sty1_cast2()
TYPE =
       ∀g:G
         .∀c:C
           .∀t1:T
             .∀t2:T
               .sty1 g c t1 t2
                 →∀v1:T
                      .∀v2:T
                        .sty0 g c v1 v2
                          →ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t2)
BODY =
        assume g: G
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: sty1 g c t1 t2
          we proceed by induction on H to prove 
             ∀v1:T
               .∀v2:T
                 .sty0 g c v1 v2
                   →ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t2)
             case sty1_sty0 : t3:T H0:sty0 g c t1 t3 ⇒
                the thesis becomes 
                ∀v1:T
                  .∀v2:T
                    .∀H1:sty0 g c v1 v2
                      .ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
                    assume v1: T
                    assume v2: T
                    suppose H1: sty0 g c v1 v2
                      (h1) by (sty1_sty0 . . . . H1) we proved sty1 g c v1 v2
                      (h2) 
                         by (sty0_cast . . . . H1 . . H0)
                         we proved sty0 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v2 t3)
                         by (sty1_sty0 . . . . previous)
sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v2 t3)
                      end of h2
                      by (ex_intro2 . . . . h1 h2)
                      we proved ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)

                      ∀v1:T
                        .∀v2:T
                          .∀H1:sty0 g c v1 v2
                            .ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
             case sty1_sing : t:T :sty1 g c t1 t t3:T H2:sty0 g c t t3 ⇒
                the thesis becomes 
                ∀v1:T
                  .∀v2:T
                    .∀H3:sty0 g c v1 v2
                      .ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
                (H1) by induction hypothesis we know 
                   ∀v1:T
                     .∀v2:T
                       .sty0 g c v1 v2
                         →ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t)
                    assume v1: T
                    assume v2: T
                    suppose H3: sty0 g c v1 v2
                      (H_x) 
                         by (H1 . . H3)

                            ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t)
                      end of H_x
                      (H4) consider H_x
                      we proceed by induction on H4 to prove ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
                         case ex_intro2 : x:T H5:sty1 g c v1 x H6:sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) x t) ⇒
                            the thesis becomes ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
                               (H_x0) 
                                  by (sty1_correct . . . . H5)
ex T λt2:T.sty0 g c x t2
                               end of H_x0
                               (H7) consider H_x0
                               we proceed by induction on H7 to prove ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
                                  case ex_intro : x0:T H8:sty0 g c x x0 ⇒
                                     the thesis becomes ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
                                        (h1) 
                                           by (sty1_sing . . . . H5 . H8)
sty1 g c v1 x0
                                        end of h1
                                        (h2) 
                                           by (sty0_cast . . . . H8 . . H2)
                                           we proved sty0 g c (THead (Flat Cast) x t) (THead (Flat Cast) x0 t3)
                                           by (sty1_sing . . . . H6 . previous)
sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) x0 t3)
                                        end of h2
                                        by (ex_intro2 . . . . h1 h2)
ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
                      we proved ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)

                      ∀v1:T
                        .∀v2:T
                          .∀H3:sty0 g c v1 v2
                            .ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t3)
          we proved 
             ∀v1:T
               .∀v2:T
                 .sty0 g c v1 v2
                   →ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t2)
       we proved 
          ∀g:G
            .∀c:C
              .∀t1:T
                .∀t2:T
                  .sty1 g c t1 t2
                    →∀v1:T
                         .∀v2:T
                           .sty0 g c v1 v2
                             →ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t2)