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

                               eq
                                 T
                                 λe:TList.<λ:TList.T> CASE e OF TNil⇒t0 | TCons t1 ⇒t1 (TCons t0 ts0)
                                 λe:TList.<λ:TList.T> CASE e OF TNil⇒t0 | TCons t1 ⇒t1 (TCons t ts)
                         end of H5
                         (h1) 
                            (H6) 
                               by (f_equal . . . . . H4)
                               we proved 
                                  eq
                                    TList
                                    <λ:TList.TList> CASE TCons t0 ts0 OF TNil⇒ts0 | TCons  t1⇒t1
                                    <λ:TList.TList> CASE TCons t ts OF TNil⇒ts0 | TCons  t1⇒t1

                                  eq
                                    TList
                                    λe:TList.<λ:TList.TList> CASE e OF TNil⇒ts0 | TCons  t1⇒t1 (TCons t0 ts0)
                                    λe:TList.<λ:TList.TList> CASE e OF TNil⇒ts0 | TCons  t1⇒t1 (TCons t ts)
                            end of H6
                            suppose H7: eq T t0 t
                               (H9) 
                                  consider H6
                                  we proved 
                                     eq
                                       TList
                                       <λ:TList.TList> CASE TCons t0 ts0 OF TNil⇒ts0 | TCons  t1⇒t1
                                       <λ:TList.TList> CASE TCons t ts OF TNil⇒ts0 | TCons  t1⇒t1
                                  that is equivalent to eq TList ts0 ts
                                  we proceed by induction on the previous result to prove tys3 g c ts u0
                                     case refl_equal : ⇒
                                        the thesis becomes the hypothesis H2
tys3 g c ts u0
                               end of H9
                               (H10) 
                                  we proceed by induction on H7 to prove ty3 g c t u0
                                     case refl_equal : ⇒
                                        the thesis becomes the hypothesis H1
ty3 g c t u0
                               end of H10
                               by (conj . . H10 H9)
                               we proved land (ty3 g c t u0) (tys3 g c ts u0)
(eq T t0 t)→(land (ty3 g c t u0) (tys3 g c ts u0))
                         end of h1
                         (h2) 
                            consider H5
                            we proved 
                               eq
                                 T
                                 <λ:TList.T> CASE TCons t0 ts0 OF TNil⇒t0 | TCons t1 ⇒t1
                                 <λ:TList.T> CASE TCons t ts OF TNil⇒t0 | TCons t1 ⇒t1
eq T t0 t
                         end of h2
                         by (h1 h2)
                         we proved land (ty3 g c t u0) (tys3 g c ts u0)
∀H4:(eq TList (TCons t0 ts0) (TCons t ts)).(land (ty3 g c t u0) (tys3 g c ts u0))
             we proved (eq TList y (TCons t ts))→(land (ty3 g c t u) (tys3 g c ts u))
          we proved 
             ∀y:TList
               .tys3 g c y u
                 →(eq TList y (TCons t ts))→(land (ty3 g c t u) (tys3 g c ts u))
          by (insert_eq . . . . previous H)
          we proved land (ty3 g c t u) (tys3 g c ts u)
       we proved 
          ∀g:G
            .∀c:C
              .∀ts:TList.∀t:T.∀u:T.(tys3 g c (TCons t ts) u)→(land (ty3 g c t u) (tys3 g c ts u))