DEFINITION ty3_correct()
TYPE =
       ∀g:G.∀c:C.∀t1:T.∀t2:T.(ty3 g c t1 t2)→(ex T λt:T.ty3 g c t2 t)
BODY =
        assume g: G
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: ty3 g c t1 t2
          we proceed by induction on H to prove ex T λt3:T.ty3 g c t2 t3
             case ty3_conv : c0:C t0:T t:T H0:ty3 g c0 t0 t u:T t3:T :ty3 g c0 u t3 :pc3 c0 t3 t0 ⇒
                the thesis becomes ex T λt4:T.ty3 g c0 t0 t4
                () by induction hypothesis we know ex T λt3:T.ty3 g c0 t t3
                () by induction hypothesis we know ex T λt4:T.ty3 g c0 t3 t4
                   by (ex_intro . . . H0)
ex T λt4:T.ty3 g c0 t0 t4
             case ty3_sort : c0:C m:nat ⇒
                the thesis becomes ex T λt:T.ty3 g c0 (TSort (next g m)) t
                   by (ty3_sort . . .)
                   we proved ty3 g c0 (TSort (next g m)) (TSort (next g (next g m)))
                   by (ex_intro . . . previous)
ex T λt:T.ty3 g c0 (TSort (next g m)) t
             case ty3_abbr : n:nat c0:C d:C u:T H0:getl n c0 (CHead d (Bind Abbr) u) t:T :ty3 g d u t ⇒
                the thesis becomes ex T λt0:T.ty3 g c0 (lift (S n) O t) t0
                (H2) by induction hypothesis we know ex T λt0:T.ty3 g d t t0
                   (H3) consider H2
                   we proceed by induction on H3 to prove ex T λt0:T.ty3 g c0 (lift (S n) O t) t0
                      case ex_intro : x:T H4:ty3 g d t x ⇒
                         the thesis becomes ex T λt0:T.ty3 g c0 (lift (S n) O t) t0
                            by (getl_drop . . . . . H0)
                            we proved drop (S n) O c0 d
                            by (ty3_lift . . . . H4 . . . previous)
                            we proved ty3 g c0 (lift (S n) O t) (lift (S n) O x)
                            by (ex_intro . . . previous)
ex T λt0:T.ty3 g c0 (lift (S n) O t) t0
ex T λt0:T.ty3 g c0 (lift (S n) O t) t0
             case ty3_abst : n:nat c0:C d:C u:T H0:getl n c0 (CHead d (Bind Abst) u) t:T H1:ty3 g d u t ⇒
                the thesis becomes ex T λt0:T.ty3 g c0 (lift (S n) O u) t0
                () by induction hypothesis we know ex T λt0:T.ty3 g d t t0
                   by (getl_drop . . . . . H0)
                   we proved drop (S n) O c0 d
                   by (ty3_lift . . . . H1 . . . previous)
                   we proved ty3 g c0 (lift (S n) O u) (lift (S n) O t)
                   by (ex_intro . . . previous)
ex T λt0:T.ty3 g c0 (lift (S n) O u) t0
             case ty3_bind : c0:C u:T t:T H0:ty3 g c0 u t b:B t0:T t3:T :ty3 g (CHead c0 (Bind b) u) t0 t3 ⇒
                the thesis becomes ex T λt4:T.ty3 g c0 (THead (Bind b) u t3) t4
                () by induction hypothesis we know ex T λt0:T.ty3 g c0 t t0
                (H3) by induction hypothesis we know ex T λt4:T.ty3 g (CHead c0 (Bind b) u) t3 t4
                   (H4) consider H3
                   we proceed by induction on H4 to prove ex T λt4:T.ty3 g c0 (THead (Bind b) u t3) t4
                      case ex_intro : x:T H5:ty3 g (CHead c0 (Bind b) u) t3 x ⇒
                         the thesis becomes ex T λt4:T.ty3 g c0 (THead (Bind b) u t3) t4
                            by (ty3_bind . . . . H0 . . . H5)
                            we proved ty3 g c0 (THead (Bind b) u t3) (THead (Bind b) u x)
                            by (ex_intro . . . previous)
ex T λt4:T.ty3 g c0 (THead (Bind b) u t3) t4
ex T λt4:T.ty3 g c0 (THead (Bind b) u t3) t4
             case ty3_appl : c0:C w:T u:T H0:ty3 g c0 w u v:T t:T :ty3 g c0 v (THead (Bind Abst) u t) ⇒
                the thesis becomes ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
                (H1) by induction hypothesis we know ex T λt:T.ty3 g c0 u t
                (H3) by induction hypothesis we know ex T λt0:T.ty3 g c0 (THead (Bind Abst) u t) t0
                   (H4) consider H1
                   we proceed by induction on H4 to prove ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
                      case ex_intro : x:T :ty3 g c0 u x ⇒
                         the thesis becomes ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
                            (H6) consider H3
                            we proceed by induction on H6 to prove ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
                               case ex_intro : x0:T H7:ty3 g c0 (THead (Bind Abst) u t) x0 ⇒
                                  the thesis becomes ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
                                     by (ty3_gen_bind . . . . . . H7)
                                     we proved 
                                        ex3_2
                                          T
                                          T
                                          λt2:T.λ:T.pc3 c0 (THead (Bind Abst) u t2) x0
                                          λ:T.λt:T.ty3 g c0 u t
                                          λt2:T.λ:T.ty3 g (CHead c0 (Bind Abst) u) t t2
                                     we proceed by induction on the previous result to prove ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
                                        case ex3_2_intro : x1:T x2:T :pc3 c0 (THead (Bind Abst) u x1) x0 H9:ty3 g c0 u x2 H10:ty3 g (CHead c0 (Bind Abst) u) t x1 ⇒
                                           the thesis becomes ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
                                              by (ty3_bind . . . . H9 . . . H10)
                                              we proved ty3 g c0 (THead (Bind Abst) u t) (THead (Bind Abst) u x1)
                                              by (ty3_appl . . . . H0 . . previous)
                                              we proved 
                                                 ty3
                                                   g
                                                   c0
                                                   THead (Flat Appl) w (THead (Bind Abst) u t)
                                                   THead (Flat Appl) w (THead (Bind Abst) u x1)
                                              by (ex_intro . . . previous)
ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
ex T λt0:T.ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0
             case ty3_cast : c0:C t0:T t3:T :ty3 g c0 t0 t3 t4:T H2:ty3 g c0 t3 t4 ⇒
                the thesis becomes ex T λt:T.ty3 g c0 (THead (Flat Cast) t4 t3) t
                () by induction hypothesis we know ex T λt:T.ty3 g c0 t3 t
                (H3) by induction hypothesis we know ex T λt:T.ty3 g c0 t4 t
                   (H4) consider H3
                   we proceed by induction on H4 to prove ex T λt:T.ty3 g c0 (THead (Flat Cast) t4 t3) t
                      case ex_intro : x:T H5:ty3 g c0 t4 x ⇒
                         the thesis becomes ex T λt:T.ty3 g c0 (THead (Flat Cast) t4 t3) t
                            by (ty3_cast . . . . H2 . H5)
                            we proved ty3 g c0 (THead (Flat Cast) t4 t3) (THead (Flat Cast) x t4)
                            by (ex_intro . . . previous)
ex T λt:T.ty3 g c0 (THead (Flat Cast) t4 t3) t
ex T λt:T.ty3 g c0 (THead (Flat Cast) t4 t3) t
          we proved ex T λt3:T.ty3 g c t2 t3
       we proved ∀g:G.∀c:C.∀t1:T.∀t2:T.(ty3 g c t1 t2)→(ex T λt3:T.ty3 g c t2 t3)