DEFINITION sty1_cnt()
TYPE =
       ∀g:G.∀c:C.∀t1:T.∀t:T.(sty0 g c t1 t)→(ex2 T λt2:T.sty1 g c t1 t2 λt2:T.cnt t2)
BODY =
        assume g: G
        assume c: C
        assume t1: T
        assume t: T
        suppose H: sty0 g c t1 t
          we proceed by induction on H to prove ex2 T λt3:T.sty1 g c t1 t3 λt3:T.cnt t3
             case sty0_sort : c0:C n:nat ⇒
                the thesis becomes ex2 T λt2:T.sty1 g c0 (TSort n) t2 λt2:T.cnt t2
                   (h1) 
                      by (sty0_sort . . .)
                      we proved sty0 g c0 (TSort n) (TSort (next g n))
                      by (sty1_sty0 . . . . previous)
sty1 g c0 (TSort n) (TSort (next g n))
                   end of h1
                   (h2) 
                      by (cnt_sort .)
cnt (TSort (next g n))
                   end of h2
                   by (ex_intro2 . . . . h1 h2)
ex2 T λt2:T.sty1 g c0 (TSort n) t2 λt2:T.cnt t2
             case sty0_abbr : c0:C d:C v:T i:nat H0:getl i c0 (CHead d (Bind Abbr) v) w:T :sty0 g d v w ⇒
                the thesis becomes ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
                (H2) by induction hypothesis we know ex2 T λt2:T.sty1 g d v t2 λt2:T.cnt t2
                   (H3) consider H2
                   we proceed by induction on H3 to prove ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
                      case ex_intro2 : x:T H4:sty1 g d v x H5:cnt x ⇒
                         the thesis becomes ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
                            (h1) 
                               by (sty1_abbr . . . . . H0 . H4)
sty1 g c0 (TLRef i) (lift (S i) O x)
                            end of h1
                            (h2) 
                               by (cnt_lift . H5 . .)
cnt (lift (S i) O x)
                            end of h2
                            by (ex_intro2 . . . . h1 h2)
ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
             case sty0_abst : c0:C d:C v:T i:nat H0:getl i c0 (CHead d (Bind Abst) v) w:T H1:sty0 g d v w ⇒
                the thesis becomes ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
                (H2) by induction hypothesis we know ex2 T λt2:T.sty1 g d v t2 λt2:T.cnt t2
                   (H3) consider H2
                   we proceed by induction on H3 to prove ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
                      case ex_intro2 : x:T H4:sty1 g d v x H5:cnt x ⇒
                         the thesis becomes ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
                            (h1) 
                               (h1) 
                                  by (sty0_abst . . . . . H0 . H1)
                                  we proved sty0 g c0 (TLRef i) (lift (S i) O v)
                                  by (sty1_sty0 . . . . previous)
sty1 g c0 (TLRef i) (lift (S i) O v)
                               end of h1
                               (h2) 
                                  by (getl_drop . . . . . H0)
                                  we proved drop (S i) O c0 d
                                  by (sty1_lift . . . . H4 . . . previous)
sty1 g c0 (lift (S i) O v) (lift (S i) O x)
                               end of h2
                               by (sty1_trans . . . . h1 . h2)
sty1 g c0 (TLRef i) (lift (S i) O x)
                            end of h1
                            (h2) 
                               by (cnt_lift . H5 . .)
cnt (lift (S i) O x)
                            end of h2
                            by (ex_intro2 . . . . h1 h2)
ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
ex2 T λt2:T.sty1 g c0 (TLRef i) t2 λt2:T.cnt t2
             case sty0_bind : b:B c0:C v:T t2:T t3:T :sty0 g (CHead c0 (Bind b) v) t2 t3 ⇒
                the thesis becomes ex2 T λt4:T.sty1 g c0 (THead (Bind b) v t2) t4 λt4:T.cnt t4
                (H1) by induction hypothesis we know ex2 T λt4:T.sty1 g (CHead c0 (Bind b) v) t2 t4 λt4:T.cnt t4
                   (H2) consider H1
                   we proceed by induction on H2 to prove ex2 T λt4:T.sty1 g c0 (THead (Bind b) v t2) t4 λt4:T.cnt t4
                      case ex_intro2 : x:T H3:sty1 g (CHead c0 (Bind b) v) t2 x H4:cnt x ⇒
                         the thesis becomes ex2 T λt4:T.sty1 g c0 (THead (Bind b) v t2) t4 λt4:T.cnt t4
                            (h1) 
                               by (sty1_bind . . . . . . H3)
sty1 g c0 (THead (Bind b) v t2) (THead (Bind b) v x)
                            end of h1
                            (h2) 
                               by (cnt_head . H4 . .)
cnt (THead (Bind b) v x)
                            end of h2
                            by (ex_intro2 . . . . h1 h2)
ex2 T λt4:T.sty1 g c0 (THead (Bind b) v t2) t4 λt4:T.cnt t4
ex2 T λt4:T.sty1 g c0 (THead (Bind b) v t2) t4 λt4:T.cnt t4
             case sty0_appl : c0:C v:T t2:T t3:T :sty0 g c0 t2 t3 ⇒
                the thesis becomes ex2 T λt4:T.sty1 g c0 (THead (Flat Appl) v t2) t4 λt4:T.cnt t4
                (H1) by induction hypothesis we know ex2 T λt4:T.sty1 g c0 t2 t4 λt4:T.cnt t4
                   (H2) consider H1
                   we proceed by induction on H2 to prove ex2 T λt4:T.sty1 g c0 (THead (Flat Appl) v t2) t4 λt4:T.cnt t4
                      case ex_intro2 : x:T H3:sty1 g c0 t2 x H4:cnt x ⇒
                         the thesis becomes ex2 T λt4:T.sty1 g c0 (THead (Flat Appl) v t2) t4 λt4:T.cnt t4
                            (h1) 
                               by (sty1_appl . . . . . H3)
sty1 g c0 (THead (Flat Appl) v t2) (THead (Flat Appl) v x)
                            end of h1
                            (h2) 
                               by (cnt_head . H4 . .)
cnt (THead (Flat Appl) v x)
                            end of h2
                            by (ex_intro2 . . . . h1 h2)
ex2 T λt4:T.sty1 g c0 (THead (Flat Appl) v t2) t4 λt4:T.cnt t4
ex2 T λt4:T.sty1 g c0 (THead (Flat Appl) v t2) t4 λt4:T.cnt t4
             case sty0_cast : c0:C v1:T v2:T H0:sty0 g c0 v1 v2 t2:T t3:T :sty0 g c0 t2 t3 ⇒
                the thesis becomes ex2 T λt4:T.sty1 g c0 (THead (Flat Cast) v1 t2) t4 λt4:T.cnt t4
                () by induction hypothesis we know ex2 T λt2:T.sty1 g c0 v1 t2 λt2:T.cnt t2
                (H3) by induction hypothesis we know ex2 T λt4:T.sty1 g c0 t2 t4 λt4:T.cnt t4
                   (H4) consider H3
                   we proceed by induction on H4 to prove ex2 T λt4:T.sty1 g c0 (THead (Flat Cast) v1 t2) t4 λt4:T.cnt t4
                      case ex_intro2 : x:T H5:sty1 g c0 t2 x H6:cnt x ⇒
                         the thesis becomes ex2 T λt4:T.sty1 g c0 (THead (Flat Cast) v1 t2) t4 λt4:T.cnt t4
                            (H_x) 
                               by (sty1_cast2 . . . . H5 . . H0)
ex2 T λv3:T.sty1 g c0 v1 v3 λv3:T.sty1 g c0 (THead (Flat Cast) v1 t2) (THead (Flat Cast) v3 x)
                            end of H_x
                            (H7) consider H_x
                            we proceed by induction on H7 to prove ex2 T λt4:T.sty1 g c0 (THead (Flat Cast) v1 t2) t4 λt4:T.cnt t4
                               case ex_intro2 : x0:T :sty1 g c0 v1 x0 H9:sty1 g c0 (THead (Flat Cast) v1 t2) (THead (Flat Cast) x0 x) ⇒
                                  the thesis becomes ex2 T λt4:T.sty1 g c0 (THead (Flat Cast) v1 t2) t4 λt4:T.cnt t4
                                     by (cnt_head . H6 . .)
                                     we proved cnt (THead (Flat Cast) x0 x)
                                     by (ex_intro2 . . . . H9 previous)
ex2 T λt4:T.sty1 g c0 (THead (Flat Cast) v1 t2) t4 λt4:T.cnt t4
ex2 T λt4:T.sty1 g c0 (THead (Flat Cast) v1 t2) t4 λt4:T.cnt t4
ex2 T λt4:T.sty1 g c0 (THead (Flat Cast) v1 t2) t4 λt4:T.cnt t4
          we proved ex2 T λt3:T.sty1 g c t1 t3 λt3:T.cnt t3
       we proved ∀g:G.∀c:C.∀t1:T.∀t:T.(sty0 g c t1 t)→(ex2 T λt3:T.sty1 g c t1 t3 λt3:T.cnt t3)