DEFINITION lifts_inj()
TYPE =
       ∀xs:TList
         .∀ts:TList
           .∀h:nat
             .∀d:nat
               .(eq TList (lifts h d xs) (lifts h d ts))→(eq TList xs ts)
BODY =
       assume xs: TList
          we proceed by induction on xs to prove 
             ∀ts:TList
               .∀h:nat
                 .∀d:nat
                   .(eq TList (lifts h d xs) (lifts h d ts))→(eq TList xs ts)
             case TNil : ⇒
                the thesis becomes 
                ∀ts:TList
                  .∀h:nat
                    .∀d:nat
                      .eq TList (lifts h d TNil) (lifts h d ts)
                        →eq TList TNil ts
                   assume ts: TList
                      we proceed by induction on ts to prove 
                         ∀h:nat
                           .∀d:nat
                             .eq TList (lifts h d TNil) (lifts h d ts)
                               →eq TList TNil ts
                         case TNil : ⇒
                            the thesis becomes 
                            nat
                              →(nat
                                   →(eq TList (lifts __2 __1 TNil) (lifts __2 __1 TNil)
                                        →eq TList TNil TNil))
                                assume : nat
                                assume : nat
                                  we must prove 
                                        eq TList (lifts __2 __1 TNil) (lifts __2 __1 TNil)
                                          →eq TList TNil TNil
                                  or equivalently (eq TList TNil TNil)→(eq TList TNil TNil)
                                  suppose : eq TList TNil TNil
                                     by (refl_equal . .)
                                     we proved eq TList TNil TNil
                                  we proved (eq TList TNil TNil)→(eq TList TNil TNil)
                                  that is equivalent to 
                                     eq TList (lifts __2 __1 TNil) (lifts __2 __1 TNil)
                                       →eq TList TNil TNil

                                  nat
                                    →(nat
                                         →(eq TList (lifts __2 __1 TNil) (lifts __2 __1 TNil)
                                              →eq TList TNil TNil))
                         case TCons : t:T t0:TList ⇒
                            the thesis becomes 
                            ∀h:nat
                              .∀d:nat
                                .eq TList (lifts h d TNil) (lifts h d (TCons t t0))
                                  →eq TList TNil (TCons t t0)
                            () by induction hypothesis we know ∀h:nat.∀d:nat.(eq TList TNil (lifts h d t0))→(eq TList TNil t0)
                                assume h: nat
                                assume d: nat
                                  we must prove 
                                        eq TList (lifts h d TNil) (lifts h d (TCons t t0))
                                          →eq TList TNil (TCons t t0)
                                  or equivalently 
                                        eq TList TNil (TCons (lift h d t) (lifts h d t0))
                                          →eq TList TNil (TCons t t0)
                                  suppose H0: eq TList TNil (TCons (lift h d t) (lifts h d t0))
                                     (H1) 
                                        we proceed by induction on H0 to prove 
                                           <λ:TList.Prop>
                                             CASE TCons (lift h d t) (lifts h d t0) 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 (lift h d t) (lifts h d t0) OF
                                               TNil⇒True
                                             | TCons  ⇒False
                                     end of H1
                                     consider H1
                                     we proved 
                                        <λ:TList.Prop>
                                          CASE TCons (lift h d t) (lifts h d t0) OF
                                            TNil⇒True
                                          | TCons  ⇒False
                                     that is equivalent to False
                                     we proceed by induction on the previous result to prove eq TList TNil (TCons t t0)
                                     we proved eq TList TNil (TCons t t0)
                                  we proved 
                                     eq TList TNil (TCons (lift h d t) (lifts h d t0))
                                       →eq TList TNil (TCons t t0)
                                  that is equivalent to 
                                     eq TList (lifts h d TNil) (lifts h d (TCons t t0))
                                       →eq TList TNil (TCons t t0)

                                  ∀h:nat
                                    .∀d:nat
                                      .eq TList (lifts h d TNil) (lifts h d (TCons t t0))
                                        →eq TList TNil (TCons t t0)
                      we proved 
                         ∀h:nat
                           .∀d:nat
                             .eq TList (lifts h d TNil) (lifts h d ts)
                               →eq TList TNil ts

                      ∀ts:TList
                        .∀h:nat
                          .∀d:nat
                            .eq TList (lifts h d TNil) (lifts h d ts)
                              →eq TList TNil ts
             case TCons : t:T t0:TList ⇒
                the thesis becomes 
                ∀ts:TList
                  .∀h:nat
                    .∀d:nat
                      .eq TList (lifts h d (TCons t t0)) (lifts h d ts)
                        →eq TList (TCons t t0) ts
                (H) by induction hypothesis we know 
                   ∀ts:TList
                     .∀h:nat
                       .∀d:nat.(eq TList (lifts h d t0) (lifts h d ts))→(eq TList t0 ts)
                   assume ts: TList
                      we proceed by induction on ts to prove 
                         ∀h:nat
                           .∀d:nat
                             .eq TList (lifts h d (TCons t t0)) (lifts h d ts)
                               →eq TList (TCons t t0) ts
                         case TNil : ⇒
                            the thesis becomes 
                            ∀h:nat
                              .∀d:nat
                                .eq TList (lifts h d (TCons t t0)) (lifts h d TNil)
                                  →eq TList (TCons t t0) TNil
                                assume h: nat
                                assume d: nat
                                  we must prove 
                                        eq TList (lifts h d (TCons t t0)) (lifts h d TNil)
                                          →eq TList (TCons t t0) TNil
                                  or equivalently 
                                        eq TList (TCons (lift h d t) (lifts h d t0)) TNil
                                          →eq TList (TCons t t0) TNil
                                  suppose H0: eq TList (TCons (lift h d t) (lifts h d t0)) TNil
                                     (H1) 
                                        we proceed by induction on H0 to prove <λ:TList.Prop> CASE TNil OF TNil⇒False | TCons  ⇒True
                                           case refl_equal : ⇒
                                              the thesis becomes 
                                              <λ:TList.Prop>
                                                CASE TCons (lift h d t) (lifts h d t0) OF
                                                  TNil⇒False
                                                | TCons  ⇒True
                                                 consider I
                                                 we proved True

                                                    <λ:TList.Prop>
                                                      CASE TCons (lift h d t) (lifts h d t0) OF
                                                        TNil⇒False
                                                      | TCons  ⇒True
<λ:TList.Prop> CASE TNil OF TNil⇒False | TCons  ⇒True
                                     end of H1
                                     consider H1
                                     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 eq TList (TCons t t0) TNil
                                     we proved eq TList (TCons t t0) TNil
                                  we proved 
                                     eq TList (TCons (lift h d t) (lifts h d t0)) TNil
                                       →eq TList (TCons t t0) TNil
                                  that is equivalent to 
                                     eq TList (lifts h d (TCons t t0)) (lifts h d TNil)
                                       →eq TList (TCons t t0) TNil

                                  ∀h:nat
                                    .∀d:nat
                                      .eq TList (lifts h d (TCons t t0)) (lifts h d TNil)
                                        →eq TList (TCons t t0) TNil
                         case TCons : t1:T t2:TList ⇒
                            the thesis becomes 
                            ∀h:nat
                              .∀d:nat
                                .eq TList (lifts h d (TCons t t0)) (lifts h d (TCons t1 t2))
                                  →eq TList (TCons t t0) (TCons t1 t2)
                            () by induction hypothesis we know 
                               ∀h:nat
                                 .∀d:nat
                                   .eq TList (TCons (lift h d t) (lifts h d t0)) (lifts h d t2)
                                     →eq TList (TCons t t0) t2
                                assume h: nat
                                assume d: nat
                                  we must prove 
                                        eq TList (lifts h d (TCons t t0)) (lifts h d (TCons t1 t2))
                                          →eq TList (TCons t t0) (TCons t1 t2)
                                  or equivalently 
                                        (eq
                                            TList
                                            TCons (lift h d t) (lifts h d t0)
                                            TCons (lift h d t1) (lifts h d t2))
                                          →eq TList (TCons t t0) (TCons t1 t2)
                                  suppose H1: 
                                     eq
                                       TList
                                       TCons (lift h d t) (lifts h d t0)
                                       TCons (lift h d t1) (lifts h d t2)
                                     (H2) 
                                        by (f_equal . . . . . H1)
                                        we proved 
                                           eq
                                             T
                                             <λ:TList.T>
                                               CASE TCons (lift h d t) (lifts h d t0) OF
                                                 TNil⇒
                                                     FIXlref_map{
                                                         lref_map:(nat→nat)→nat→T→T
                                                         :=λf:nat→nat
                                                           .λd0:nat
                                                             .λt3:T
                                                               .<λt4:T.T>
                                                                 CASE t3 OF
                                                                   TSort n⇒TSort n
                                                                 | TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
                                                                 | THead k u t4⇒THead k (lref_map f d0 u) (lref_map f (s k d0) t4)
                                                         }
                                                       λx:nat.plus x h
                                                       d
                                                       t
                                               | TCons t3 ⇒t3
                                             <λ:TList.T>
                                               CASE TCons (lift h d t1) (lifts h d t2) OF
                                                 TNil⇒
                                                     FIXlref_map{
                                                         lref_map:(nat→nat)→nat→T→T
                                                         :=λf:nat→nat
                                                           .λd0:nat
                                                             .λt3:T
                                                               .<λt4:T.T>
                                                                 CASE t3 OF
                                                                   TSort n⇒TSort n
                                                                 | TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
                                                                 | THead k u t4⇒THead k (lref_map f d0 u) (lref_map f (s k d0) t4)
                                                         }
                                                       λx:nat.plus x h
                                                       d
                                                       t
                                               | TCons t3 ⇒t3

                                           eq
                                             T
                                             λe:TList
                                                 .<λ:TList.T>
                                                   CASE e OF
                                                     TNil⇒
                                                         FIXlref_map{
                                                             lref_map:(nat→nat)→nat→T→T
                                                             :=λf:nat→nat
                                                               .λd0:nat
                                                                 .λt3:T
                                                                   .<λt4:T.T>
                                                                     CASE t3 OF
                                                                       TSort n⇒TSort n
                                                                     | TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
                                                                     | THead k u t4⇒THead k (lref_map f d0 u) (lref_map f (s k d0) t4)
                                                             }
                                                           λx:nat.plus x h
                                                           d
                                                           t
                                                   | TCons t3 ⇒t3
                                               TCons (lift h d t) (lifts h d t0)
                                             λe:TList
                                                 .<λ:TList.T>
                                                   CASE e OF
                                                     TNil⇒
                                                         FIXlref_map{
                                                             lref_map:(nat→nat)→nat→T→T
                                                             :=λf:nat→nat
                                                               .λd0:nat
                                                                 .λt3:T
                                                                   .<λt4:T.T>
                                                                     CASE t3 OF
                                                                       TSort n⇒TSort n
                                                                     | TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
                                                                     | THead k u t4⇒THead k (lref_map f d0 u) (lref_map f (s k d0) t4)
                                                             }
                                                           λx:nat.plus x h
                                                           d
                                                           t
                                                   | TCons t3 ⇒t3
                                               TCons (lift h d t1) (lifts h d t2)
                                     end of H2
                                     (h1) 
                                        (H3) 
                                           by (f_equal . . . . . H1)
                                           we proved 
                                              eq
                                                TList
                                                <λ:TList.TList>
                                                  CASE TCons (lift h d t) (lifts h d t0) OF
                                                    TNil⇒
                                                        FIXlifts{
                                                            lifts:nat→nat→TList→TList
                                                            :=λh0:nat
                                                              .λd0:nat
                                                                .λts0:TList
                                                                  .<λt3:TList.TList>
                                                                    CASE ts0 OF
                                                                      TNil⇒TNil
                                                                    | TCons t3 ts1⇒TCons (lift h0 d0 t3) (lifts h0 d0 ts1)
                                                            }
                                                          h
                                                          d
                                                          t0
                                                  | TCons  t3⇒t3
                                                <λ:TList.TList>
                                                  CASE TCons (lift h d t1) (lifts h d t2) OF
                                                    TNil⇒
                                                        FIXlifts{
                                                            lifts:nat→nat→TList→TList
                                                            :=λh0:nat
                                                              .λd0:nat
                                                                .λts0:TList
                                                                  .<λt3:TList.TList>
                                                                    CASE ts0 OF
                                                                      TNil⇒TNil
                                                                    | TCons t3 ts1⇒TCons (lift h0 d0 t3) (lifts h0 d0 ts1)
                                                            }
                                                          h
                                                          d
                                                          t0
                                                  | TCons  t3⇒t3

                                              eq
                                                TList
                                                λe:TList
                                                    .<λ:TList.TList>
                                                      CASE e OF
                                                        TNil⇒
                                                            FIXlifts{
                                                                lifts:nat→nat→TList→TList
                                                                :=λh0:nat
                                                                  .λd0:nat
                                                                    .λts0:TList
                                                                      .<λt3:TList.TList>
                                                                        CASE ts0 OF
                                                                          TNil⇒TNil
                                                                        | TCons t3 ts1⇒TCons (lift h0 d0 t3) (lifts h0 d0 ts1)
                                                                }
                                                              h
                                                              d
                                                              t0
                                                      | TCons  t3⇒t3
                                                  TCons (lift h d t) (lifts h d t0)
                                                λe:TList
                                                    .<λ:TList.TList>
                                                      CASE e OF
                                                        TNil⇒
                                                            FIXlifts{
                                                                lifts:nat→nat→TList→TList
                                                                :=λh0:nat
                                                                  .λd0:nat
                                                                    .λts0:TList
                                                                      .<λt3:TList.TList>
                                                                        CASE ts0 OF
                                                                          TNil⇒TNil
                                                                        | TCons t3 ts1⇒TCons (lift h0 d0 t3) (lifts h0 d0 ts1)
                                                                }
                                                              h
                                                              d
                                                              t0
                                                      | TCons  t3⇒t3
                                                  TCons (lift h d t1) (lifts h d t2)
                                        end of H3
                                        suppose H4: eq T (lift h d t) (lift h d t1)
                                           by (lift_inj . . . . H4)
                                           we proved eq T t t1
                                           we proceed by induction on the previous result to prove eq TList (TCons t t0) (TCons t1 t2)
                                              case refl_equal : ⇒
                                                 the thesis becomes eq TList (TCons t t0) (TCons t t2)
                                                    (h1) 
                                                       by (refl_equal . .)
eq T t t
                                                    end of h1
                                                    (h2) 
                                                       consider H3
                                                       we proved 
                                                          eq
                                                            TList
                                                            <λ:TList.TList>
                                                              CASE TCons (lift h d t) (lifts h d t0) OF
                                                                TNil⇒
                                                                    FIXlifts{
                                                                        lifts:nat→nat→TList→TList
                                                                        :=λh0:nat
                                                                          .λd0:nat
                                                                            .λts0:TList
                                                                              .<λt3:TList.TList>
                                                                                CASE ts0 OF
                                                                                  TNil⇒TNil
                                                                                | TCons t3 ts1⇒TCons (lift h0 d0 t3) (lifts h0 d0 ts1)
                                                                        }
                                                                      h
                                                                      d
                                                                      t0
                                                              | TCons  t3⇒t3
                                                            <λ:TList.TList>
                                                              CASE TCons (lift h d t1) (lifts h d t2) OF
                                                                TNil⇒
                                                                    FIXlifts{
                                                                        lifts:nat→nat→TList→TList
                                                                        :=λh0:nat
                                                                          .λd0:nat
                                                                            .λts0:TList
                                                                              .<λt3:TList.TList>
                                                                                CASE ts0 OF
                                                                                  TNil⇒TNil
                                                                                | TCons t3 ts1⇒TCons (lift h0 d0 t3) (lifts h0 d0 ts1)
                                                                        }
                                                                      h
                                                                      d
                                                                      t0
                                                              | TCons  t3⇒t3
                                                       that is equivalent to eq TList (lifts h d t0) (lifts h d t2)
                                                       by (H . . . previous)
eq TList t0 t2
                                                    end of h2
                                                    by (f_equal2 . . . . . . . . h1 h2)
eq TList (TCons t t0) (TCons t t2)
                                           we proved eq TList (TCons t t0) (TCons t1 t2)

                                           eq T (lift h d t) (lift h d t1)
                                             →eq TList (TCons t t0) (TCons t1 t2)
                                     end of h1
                                     (h2) 
                                        consider H2
                                        we proved 
                                           eq
                                             T
                                             <λ:TList.T>
                                               CASE TCons (lift h d t) (lifts h d t0) OF
                                                 TNil⇒
                                                     FIXlref_map{
                                                         lref_map:(nat→nat)→nat→T→T
                                                         :=λf:nat→nat
                                                           .λd0:nat
                                                             .λt3:T
                                                               .<λt4:T.T>
                                                                 CASE t3 OF
                                                                   TSort n⇒TSort n
                                                                 | TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
                                                                 | THead k u t4⇒THead k (lref_map f d0 u) (lref_map f (s k d0) t4)
                                                         }
                                                       λx:nat.plus x h
                                                       d
                                                       t
                                               | TCons t3 ⇒t3
                                             <λ:TList.T>
                                               CASE TCons (lift h d t1) (lifts h d t2) OF
                                                 TNil⇒
                                                     FIXlref_map{
                                                         lref_map:(nat→nat)→nat→T→T
                                                         :=λf:nat→nat
                                                           .λd0:nat
                                                             .λt3:T
                                                               .<λt4:T.T>
                                                                 CASE t3 OF
                                                                   TSort n⇒TSort n
                                                                 | TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
                                                                 | THead k u t4⇒THead k (lref_map f d0 u) (lref_map f (s k d0) t4)
                                                         }
                                                       λx:nat.plus x h
                                                       d
                                                       t
                                               | TCons t3 ⇒t3
eq T (lift h d t) (lift h d t1)
                                     end of h2
                                     by (h1 h2)
                                     we proved eq TList (TCons t t0) (TCons t1 t2)
                                  we proved 
                                     (eq
                                         TList
                                         TCons (lift h d t) (lifts h d t0)
                                         TCons (lift h d t1) (lifts h d t2))
                                       →eq TList (TCons t t0) (TCons t1 t2)
                                  that is equivalent to 
                                     eq TList (lifts h d (TCons t t0)) (lifts h d (TCons t1 t2))
                                       →eq TList (TCons t t0) (TCons t1 t2)

                                  ∀h:nat
                                    .∀d:nat
                                      .eq TList (lifts h d (TCons t t0)) (lifts h d (TCons t1 t2))
                                        →eq TList (TCons t t0) (TCons t1 t2)
                      we proved 
                         ∀h:nat
                           .∀d:nat
                             .eq TList (lifts h d (TCons t t0)) (lifts h d ts)
                               →eq TList (TCons t t0) ts

                      ∀ts:TList
                        .∀h:nat
                          .∀d:nat
                            .eq TList (lifts h d (TCons t t0)) (lifts h d ts)
                              →eq TList (TCons t t0) ts
          we proved 
             ∀ts:TList
               .∀h:nat
                 .∀d:nat
                   .(eq TList (lifts h d xs) (lifts h d ts))→(eq TList xs ts)
       we proved 
          ∀xs:TList
            .∀ts:TList
              .∀h:nat
                .∀d:nat
                  .(eq TList (lifts h d xs) (lifts h d ts))→(eq TList xs ts)