DEFINITION iso_gen_head()
TYPE =
       ∀k:K.∀v1:T.∀t1:T.∀u2:T.(iso (THead k v1 t1) u2)→(ex_2 T T λv2:T.λt2:T.eq T u2 (THead k v2 t2))
BODY =
        assume k: K
        assume v1: T
        assume t1: T
        assume u2: T
        suppose H: iso (THead k v1 t1) u2
           assume y: T
           suppose H0: iso y u2
             we proceed by induction on H0 to prove (eq T y (THead k v1 t1))→(ex_2 T T λv2:T.λt2:T.eq T u2 (THead k v2 t2))
                case iso_sort : n1:nat n2:nat ⇒
                   the thesis becomes ∀H1:(eq T (TSort n1) (THead k v1 t1)).(ex_2 T T λv2:T.λt2:T.eq T (TSort n2) (THead k v2 t2))
                      suppose H1: eq T (TSort n1) (THead k v1 t1)
                         (H2) 
                            we proceed by induction on H1 to prove 
                               <λ:T.Prop>
                                 CASE THead k v1 t1 OF
                                   TSort ⇒True
                                 | TLRef ⇒False
                                 | THead   ⇒False
                               case refl_equal : ⇒
                                  the thesis becomes 
                                  <λ:T.Prop>
                                    CASE TSort n1 OF
                                      TSort ⇒True
                                    | TLRef ⇒False
                                    | THead   ⇒False
                                     consider I
                                     we proved True

                                        <λ:T.Prop>
                                          CASE TSort n1 OF
                                            TSort ⇒True
                                          | TLRef ⇒False
                                          | THead   ⇒False

                               <λ:T.Prop>
                                 CASE THead k v1 t1 OF
                                   TSort ⇒True
                                 | TLRef ⇒False
                                 | THead   ⇒False
                         end of H2
                         consider H2
                         we proved 
                            <λ:T.Prop>
                              CASE THead k v1 t1 OF
                                TSort ⇒True
                              | TLRef ⇒False
                              | THead   ⇒False
                         that is equivalent to False
                         we proceed by induction on the previous result to prove ex_2 T T λv2:T.λt2:T.eq T (TSort n2) (THead k v2 t2)
                         we proved ex_2 T T λv2:T.λt2:T.eq T (TSort n2) (THead k v2 t2)
∀H1:(eq T (TSort n1) (THead k v1 t1)).(ex_2 T T λv2:T.λt2:T.eq T (TSort n2) (THead k v2 t2))
                case iso_lref : i1:nat i2:nat ⇒
                   the thesis becomes ∀H1:(eq T (TLRef i1) (THead k v1 t1)).(ex_2 T T λv2:T.λt2:T.eq T (TLRef i2) (THead k v2 t2))
                      suppose H1: eq T (TLRef i1) (THead k v1 t1)
                         (H2) 
                            we proceed by induction on H1 to prove 
                               <λ:T.Prop>
                                 CASE THead k v1 t1 OF
                                   TSort ⇒False
                                 | TLRef ⇒True
                                 | THead   ⇒False
                               case refl_equal : ⇒
                                  the thesis becomes 
                                  <λ:T.Prop>
                                    CASE TLRef i1 OF
                                      TSort ⇒False
                                    | TLRef ⇒True
                                    | THead   ⇒False
                                     consider I
                                     we proved True

                                        <λ:T.Prop>
                                          CASE TLRef i1 OF
                                            TSort ⇒False
                                          | TLRef ⇒True
                                          | THead   ⇒False

                               <λ:T.Prop>
                                 CASE THead k v1 t1 OF
                                   TSort ⇒False
                                 | TLRef ⇒True
                                 | THead   ⇒False
                         end of H2
                         consider H2
                         we proved 
                            <λ:T.Prop>
                              CASE THead k v1 t1 OF
                                TSort ⇒False
                              | TLRef ⇒True
                              | THead   ⇒False
                         that is equivalent to False
                         we proceed by induction on the previous result to prove ex_2 T T λv2:T.λt2:T.eq T (TLRef i2) (THead k v2 t2)
                         we proved ex_2 T T λv2:T.λt2:T.eq T (TLRef i2) (THead k v2 t2)
∀H1:(eq T (TLRef i1) (THead k v1 t1)).(ex_2 T T λv2:T.λt2:T.eq T (TLRef i2) (THead k v2 t2))
                case iso_head : v0:T v2:T t0:T t2:T k0:K ⇒
                   the thesis becomes ∀H1:(eq T (THead k0 v0 t0) (THead k v1 t1)).(ex_2 T T λv3:T.λt3:T.eq T (THead k0 v2 t2) (THead k v3 t3))
                      suppose H1: eq T (THead k0 v0 t0) (THead k v1 t1)
                         (H2) 
                            by (f_equal . . . . . H1)
                            we proved 
                               eq
                                 K
                                 <λ:T.K> CASE THead k0 v0 t0 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1  ⇒k1
                                 <λ:T.K> CASE THead k v1 t1 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1  ⇒k1

                               eq
                                 K
                                 λe:T.<λ:T.K> CASE e OF TSort ⇒k0 | TLRef ⇒k0 | THead k1  ⇒k1 (THead k0 v0 t0)
                                 λe:T.<λ:T.K> CASE e OF TSort ⇒k0 | TLRef ⇒k0 | THead k1  ⇒k1 (THead k v1 t1)
                         end of H2
                         (h1) 
                            (H3) 
                               by (f_equal . . . . . H1)
                               we proved 
                                  eq
                                    T
                                    <λ:T.T> CASE THead k0 v0 t0 OF TSort ⇒v0 | TLRef ⇒v0 | THead  t ⇒t
                                    <λ:T.T> CASE THead k v1 t1 OF TSort ⇒v0 | TLRef ⇒v0 | THead  t ⇒t

                                  eq
                                    T
                                    λe:T.<λ:T.T> CASE e OF TSort ⇒v0 | TLRef ⇒v0 | THead  t ⇒t (THead k0 v0 t0)
                                    λe:T.<λ:T.T> CASE e OF TSort ⇒v0 | TLRef ⇒v0 | THead  t ⇒t (THead k v1 t1)
                            end of H3
                            () 
                               consider H3
                               we proved 
                                  eq
                                    T
                                    <λ:T.T> CASE THead k0 v0 t0 OF TSort ⇒v0 | TLRef ⇒v0 | THead  t ⇒t
                                    <λ:T.T> CASE THead k v1 t1 OF TSort ⇒v0 | TLRef ⇒v0 | THead  t ⇒t
eq T v0 v1
                            end of 
                            suppose H6: eq K k0 k
                               by (refl_equal . .)
                               we proved eq T (THead k v2 t2) (THead k v2 t2)
                               by (ex_2_intro . . . . . previous)
                               we proved ex_2 T T λv3:T.λt3:T.eq T (THead k v2 t2) (THead k v3 t3)
                               by (eq_ind_r . . . previous . H6)
                               we proved ex_2 T T λv3:T.λt3:T.eq T (THead k0 v2 t2) (THead k v3 t3)
(eq K k0 k)→(ex_2 T T λv3:T.λt3:T.eq T (THead k0 v2 t2) (THead k v3 t3))
                         end of h1
                         (h2) 
                            consider H2
                            we proved 
                               eq
                                 K
                                 <λ:T.K> CASE THead k0 v0 t0 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1  ⇒k1
                                 <λ:T.K> CASE THead k v1 t1 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1  ⇒k1
eq K k0 k
                         end of h2
                         by (h1 h2)
                         we proved ex_2 T T λv3:T.λt3:T.eq T (THead k0 v2 t2) (THead k v3 t3)
∀H1:(eq T (THead k0 v0 t0) (THead k v1 t1)).(ex_2 T T λv3:T.λt3:T.eq T (THead k0 v2 t2) (THead k v3 t3))
             we proved (eq T y (THead k v1 t1))→(ex_2 T T λv2:T.λt2:T.eq T u2 (THead k v2 t2))
          we proved 
             ∀y:T
               .(iso y u2)→(eq T y (THead k v1 t1))→(ex_2 T T λv2:T.λt2:T.eq T u2 (THead k v2 t2))
          by (insert_eq . . . . previous H)
          we proved ex_2 T T λv2:T.λt2:T.eq T u2 (THead k v2 t2)
       we proved ∀k:K.∀v1:T.∀t1:T.∀u2:T.(iso (THead k v1 t1) u2)→(ex_2 T T λv2:T.λt2:T.eq T u2 (THead k v2 t2))