DEFINITION tys3_gen_nil()
TYPE =
       ∀g:G.∀c:C.∀u:T.(tys3 g c TNil u)→(ex T λu0:T.ty3 g c u u0)
BODY =
        assume g: G
        assume c: C
        assume u: T
        suppose H: tys3 g c TNil u
           assume y: TList
           suppose H0: tys3 g c y u
             we proceed by induction on H0 to prove (eq TList y TNil)→(ex T λu0:T.ty3 g c u u0)
                case tys3_nil : u0:T u1:T H1:ty3 g c u0 u1 ⇒
                   the thesis becomes (eq TList TNil TNil)→(ex T λu2:T.ty3 g c u0 u2)
                      suppose : eq TList TNil TNil
                         by (ex_intro . . . H1)
                         we proved ex T λu2:T.ty3 g c u0 u2
(eq TList TNil TNil)→(ex T λu2:T.ty3 g c u0 u2)
                case tys3_cons : t:T u0:T :ty3 g c t u0 ts:TList :tys3 g c ts u0 ⇒
                   the thesis becomes ∀H4:(eq TList (TCons t ts) TNil).(ex T λu1:T.ty3 g c u0 u1)
                   () by induction hypothesis we know (eq TList ts TNil)→(ex T λu1:T.ty3 g c u0 u1)
                      suppose H4: eq TList (TCons t ts) TNil
                         (H5) 
                            we proceed by induction on H4 to prove <λ:TList.Prop> CASE TNil OF TNil⇒False | TCons  ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:TList.Prop> CASE TCons t ts OF TNil⇒False | TCons  ⇒True
                                     consider I
                                     we proved True
<λ:TList.Prop> CASE TCons t ts OF TNil⇒False | TCons  ⇒True
<λ:TList.Prop> CASE TNil OF TNil⇒False | TCons  ⇒True
                         end of H5
                         consider H5
                         we proved <λ:TList.Prop> CASE TNil OF TNil⇒False | TCons  ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove ex T λu1:T.ty3 g c u0 u1
                         we proved ex T λu1:T.ty3 g c u0 u1
∀H4:(eq TList (TCons t ts) TNil).(ex T λu1:T.ty3 g c u0 u1)
             we proved (eq TList y TNil)→(ex T λu0:T.ty3 g c u u0)
          we proved ∀y:TList.(tys3 g c y u)→(eq TList y TNil)→(ex T λu0:T.ty3 g c u u0)
          by (insert_eq . . . . previous H)
          we proved ex T λu0:T.ty3 g c u u0
       we proved ∀g:G.∀c:C.∀u:T.(tys3 g c TNil u)→(ex T λu0:T.ty3 g c u u0)