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

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

                               <λ:T.Prop>
                                 CASE TLRef n1 OF
                                   TSort ⇒True
                                 | TLRef ⇒False
                                 | THead   ⇒False
                         end of H2
                         consider H2
                         we proved 
                            <λ:T.Prop>
                              CASE TLRef n1 OF
                                TSort ⇒True
                              | TLRef ⇒False
                              | THead   ⇒False
                         that is equivalent to False
                         we proceed by induction on the previous result to prove ex nat λn3:nat.eq T (TSort n2) (TLRef n3)
                         we proved ex nat λn3:nat.eq T (TSort n2) (TLRef n3)

                         ∀H1:(eq T (TSort n0) (TLRef n1)).(ex nat λn3:nat.eq T (TSort n2) (TLRef n3))
                case iso_lref : i1:nat i2:nat ⇒
                   the thesis becomes 
                   ∀H1:(eq T (TLRef i1) (TLRef n1)).(ex nat λn2:nat.eq T (TLRef i2) (TLRef n2))
                      suppose H1: eq T (TLRef i1) (TLRef n1)
                         by (refl_equal . .)
                         we proved eq T (TLRef i2) (TLRef i2)
                         by (ex_intro . . . previous)
                         we proved ex nat λn2:nat.eq T (TLRef i2) (TLRef n2)

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

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

                               <λ:T.Prop>
                                 CASE TLRef n1 OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                         end of H2
                         consider H2
                         we proved 
                            <λ:T.Prop>
                              CASE TLRef n1 OF
                                TSort ⇒False
                              | TLRef ⇒False
                              | THead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove ex nat λn2:nat.eq T (THead k v2 t2) (TLRef n2)
                         we proved ex nat λn2:nat.eq T (THead k v2 t2) (TLRef n2)

                         ∀H1:eq T (THead k v1 t1) (TLRef n1)
                           .ex nat λn2:nat.eq T (THead k v2 t2) (TLRef n2)
             we proved (eq T y (TLRef n1))→(ex nat λn2:nat.eq T u2 (TLRef n2))
          we proved 
             ∀y:T
               .iso y u2
                 →(eq T y (TLRef n1))→(ex nat λn2:nat.eq T u2 (TLRef n2))
          by (insert_eq . . . . previous H)
          we proved ex nat λn2:nat.eq T u2 (TLRef n2)
       we proved ∀u2:T.∀n1:nat.(iso (TLRef n1) u2)→(ex nat λn2:nat.eq T u2 (TLRef n2))