+theorem lifts_inj:
+ \forall (xs: TList).(\forall (ts: TList).(\forall (h: nat).(\forall (d:
+nat).((eq TList (lifts h d xs) (lifts h d ts)) \to (eq TList xs ts)))))
+\def
+ \lambda (xs: TList).(TList_ind (\lambda (t: TList).(\forall (ts:
+TList).(\forall (h: nat).(\forall (d: nat).((eq TList (lifts h d t) (lifts h
+d ts)) \to (eq TList t ts)))))) (\lambda (ts: TList).(TList_ind (\lambda (t:
+TList).(\forall (h: nat).(\forall (d: nat).((eq TList (lifts h d TNil) (lifts
+h d t)) \to (eq TList TNil t))))) (\lambda (_: nat).(\lambda (_:
+nat).(\lambda (_: (eq TList TNil TNil)).(refl_equal TList TNil)))) (\lambda
+(t: T).(\lambda (t0: TList).(\lambda (_: ((\forall (h: nat).(\forall (d:
+nat).((eq TList TNil (lifts h d t0)) \to (eq TList TNil t0)))))).(\lambda (h:
+nat).(\lambda (d: nat).(\lambda (H0: (eq TList TNil (TCons (lift h d t)
+(lifts h d t0)))).(let H1 \def (eq_ind TList TNil (\lambda (ee: TList).(match
+ee in TList return (\lambda (_: TList).Prop) with [TNil \Rightarrow True |
+(TCons _ _) \Rightarrow False])) I (TCons (lift h d t) (lifts h d t0)) H0) in
+(False_ind (eq TList TNil (TCons t t0)) H1)))))))) ts)) (\lambda (t:
+T).(\lambda (t0: TList).(\lambda (H: ((\forall (ts: TList).(\forall (h:
+nat).(\forall (d: nat).((eq TList (lifts h d t0) (lifts h d ts)) \to (eq
+TList t0 ts))))))).(\lambda (ts: TList).(TList_ind (\lambda (t1:
+TList).(\forall (h: nat).(\forall (d: nat).((eq TList (lifts h d (TCons t
+t0)) (lifts h d t1)) \to (eq TList (TCons t t0) t1))))) (\lambda (h:
+nat).(\lambda (d: nat).(\lambda (H0: (eq TList (TCons (lift h d t) (lifts h d
+t0)) TNil)).(let H1 \def (eq_ind TList (TCons (lift h d t) (lifts h d t0))
+(\lambda (ee: TList).(match ee in TList return (\lambda (_: TList).Prop) with
+[TNil \Rightarrow False | (TCons _ _) \Rightarrow True])) I TNil H0) in
+(False_ind (eq TList (TCons t t0) TNil) H1))))) (\lambda (t1: T).(\lambda
+(t2: TList).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq TList
+(TCons (lift h d t) (lifts h d t0)) (lifts h d t2)) \to (eq TList (TCons t
+t0) t2)))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq TList
+(TCons (lift h d t) (lifts h d t0)) (TCons (lift h d t1) (lifts h d
+t2)))).(let H2 \def (f_equal TList T (\lambda (e: TList).(match e in TList
+return (\lambda (_: TList).T) with [TNil \Rightarrow ((let rec lref_map (f:
+((nat \to nat))) (d0: nat) (t3: T) on t3: T \def (match t3 with [(TSort n)
+\Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d0) with
+[true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t4) \Rightarrow
+(THead k (lref_map f d0 u) (lref_map f (s k d0) t4))]) in lref_map) (\lambda
+(x: nat).(plus x h)) d t) | (TCons t3 _) \Rightarrow t3])) (TCons (lift h d
+t) (lifts h d t0)) (TCons (lift h d t1) (lifts h d t2)) H1) in ((let H3 \def
+(f_equal TList TList (\lambda (e: TList).(match e in TList return (\lambda
+(_: TList).TList) with [TNil \Rightarrow ((let rec lifts (h0: nat) (d0: nat)
+(ts0: TList) on ts0: TList \def (match ts0 with [TNil \Rightarrow TNil |
+(TCons t3 ts1) \Rightarrow (TCons (lift h0 d0 t3) (lifts h0 d0 ts1))]) in
+lifts) h d t0) | (TCons _ t3) \Rightarrow t3])) (TCons (lift h d t) (lifts h
+d t0)) (TCons (lift h d t1) (lifts h d t2)) H1) in (\lambda (H4: (eq T (lift
+h d t) (lift h d t1))).(eq_ind T t (\lambda (t3: T).(eq TList (TCons t t0)
+(TCons t3 t2))) (f_equal2 T TList TList TCons t t t0 t2 (refl_equal T t) (H
+t2 h d H3)) t1 (lift_inj t t1 h d H4)))) H2)))))))) ts))))) xs).
+