DEFINITION sty0_correct()
TYPE =
       ∀g:G.∀c:C.∀t1:T.∀t:T.(sty0 g c t1 t)→(ex T λt2:T.sty0 g c t 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 ex T λt3:T.sty0 g c t t3
             case sty0_sort : c0:C n:nat ⇒
                the thesis becomes ex T λt2:T.sty0 g c0 (TSort (next g n)) t2
                   by (sty0_sort . . .)
                   we proved sty0 g c0 (TSort (next g n)) (TSort (next g (next g n)))
                   by (ex_intro . . . previous)
ex T λt2:T.sty0 g c0 (TSort (next g n)) 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 ex T λt2:T.sty0 g c0 (lift (S i) O w) t2
                (H2) by induction hypothesis we know ex T λt2:T.sty0 g d w t2
                   (H3) consider H2
                   we proceed by induction on H3 to prove ex T λt2:T.sty0 g c0 (lift (S i) O w) t2
                      case ex_intro : x:T H4:sty0 g d w x ⇒
                         the thesis becomes ex T λt2:T.sty0 g c0 (lift (S i) O w) t2
                            by (getl_drop . . . . . H0)
                            we proved drop (S i) O c0 d
                            by (sty0_lift . . . . H4 . . . previous)
                            we proved sty0 g c0 (lift (S i) O w) (lift (S i) O x)
                            by (ex_intro . . . previous)
ex T λt2:T.sty0 g c0 (lift (S i) O w) t2
ex T λt2:T.sty0 g c0 (lift (S i) O w) 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 ex T λt2:T.sty0 g c0 (lift (S i) O v) t2
                (H2) by induction hypothesis we know ex T λt2:T.sty0 g d w t2
                   (H3) consider H2
                   we proceed by induction on H3 to prove ex T λt2:T.sty0 g c0 (lift (S i) O v) t2
                      case ex_intro : x:T :sty0 g d w x ⇒
                         the thesis becomes ex T λt2:T.sty0 g c0 (lift (S i) O v) t2
                            by (getl_drop . . . . . H0)
                            we proved drop (S i) O c0 d
                            by (sty0_lift . . . . H1 . . . previous)
                            we proved sty0 g c0 (lift (S i) O v) (lift (S i) O w)
                            by (ex_intro . . . previous)
ex T λt2:T.sty0 g c0 (lift (S i) O v) t2
ex T λt2:T.sty0 g c0 (lift (S i) O v) 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 ex T λt4:T.sty0 g c0 (THead (Bind b) v t3) t4
                (H1) by induction hypothesis we know ex T λt4:T.sty0 g (CHead c0 (Bind b) v) t3 t4
                   (H2) consider H1
                   we proceed by induction on H2 to prove ex T λt4:T.sty0 g c0 (THead (Bind b) v t3) t4
                      case ex_intro : x:T H3:sty0 g (CHead c0 (Bind b) v) t3 x ⇒
                         the thesis becomes ex T λt4:T.sty0 g c0 (THead (Bind b) v t3) t4
                            by (sty0_bind . . . . . . H3)
                            we proved sty0 g c0 (THead (Bind b) v t3) (THead (Bind b) v x)
                            by (ex_intro . . . previous)
ex T λt4:T.sty0 g c0 (THead (Bind b) v t3) t4
ex T λt4:T.sty0 g c0 (THead (Bind b) v t3) t4
             case sty0_appl : c0:C v:T t2:T t3:T :sty0 g c0 t2 t3 ⇒
                the thesis becomes ex T λt4:T.sty0 g c0 (THead (Flat Appl) v t3) t4
                (H1) by induction hypothesis we know ex T λt4:T.sty0 g c0 t3 t4
                   (H2) consider H1
                   we proceed by induction on H2 to prove ex T λt4:T.sty0 g c0 (THead (Flat Appl) v t3) t4
                      case ex_intro : x:T H3:sty0 g c0 t3 x ⇒
                         the thesis becomes ex T λt4:T.sty0 g c0 (THead (Flat Appl) v t3) t4
                            by (sty0_appl . . . . . H3)
                            we proved sty0 g c0 (THead (Flat Appl) v t3) (THead (Flat Appl) v x)
                            by (ex_intro . . . previous)
ex T λt4:T.sty0 g c0 (THead (Flat Appl) v t3) t4
ex T λt4:T.sty0 g c0 (THead (Flat Appl) v t3) t4
             case sty0_cast : c0:C v1:T v2:T :sty0 g c0 v1 v2 t2:T t3:T :sty0 g c0 t2 t3 ⇒
                the thesis becomes ex T λt4:T.sty0 g c0 (THead (Flat Cast) v2 t3) t4
                (H1) by induction hypothesis we know ex T λt2:T.sty0 g c0 v2 t2
                (H3) by induction hypothesis we know ex T λt4:T.sty0 g c0 t3 t4
                   (H4) consider H1
                   we proceed by induction on H4 to prove ex T λt4:T.sty0 g c0 (THead (Flat Cast) v2 t3) t4
                      case ex_intro : x:T H5:sty0 g c0 v2 x ⇒
                         the thesis becomes ex T λt4:T.sty0 g c0 (THead (Flat Cast) v2 t3) t4
                            (H6) consider H3
                            we proceed by induction on H6 to prove ex T λt4:T.sty0 g c0 (THead (Flat Cast) v2 t3) t4
                               case ex_intro : x0:T H7:sty0 g c0 t3 x0 ⇒
                                  the thesis becomes ex T λt4:T.sty0 g c0 (THead (Flat Cast) v2 t3) t4
                                     by (sty0_cast . . . . H5 . . H7)
                                     we proved sty0 g c0 (THead (Flat Cast) v2 t3) (THead (Flat Cast) x x0)
                                     by (ex_intro . . . previous)
ex T λt4:T.sty0 g c0 (THead (Flat Cast) v2 t3) t4
ex T λt4:T.sty0 g c0 (THead (Flat Cast) v2 t3) t4
ex T λt4:T.sty0 g c0 (THead (Flat Cast) v2 t3) t4
          we proved ex T λt3:T.sty0 g c t t3
       we proved ∀g:G.∀c:C.∀t1:T.∀t:T.(sty0 g c t1 t)→(ex T λt3:T.sty0 g c t t3)