LambdaDelta.ma and some slices of it that typecheck ok!

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta-4.ma

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta-4".

include "LambdaDelta-3.ma".

definition lref_map:
 ((nat \to nat)) \to (nat \to (T \to T))
\def
 let rec lref_map (f: ((nat \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0) \Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))]) in lref_map.

definition lift:
 nat \to (nat \to (T \to T))
\def
 \lambda (h: nat).(\lambda (i: nat).(\lambda (t: T).(lref_map (\lambda (x: nat).(plus x h)) i t))).

definition lifts:
 nat \to (nat \to (TList \to TList))
\def
 let rec lifts (h: nat) (d: nat) (ts: TList) on ts: TList \def (match ts with [TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift h d t) (lifts h d ts0))]) in lifts.

theorem lift_sort:
 \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (TSort n)) (TSort n))))
\def
 \lambda (n: nat).(\lambda (_: nat).(\lambda (_: nat).(refl_equal T (TSort n)))).

theorem lift_lref_lt:
 \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((lt n d) \to (eq T (lift h d (TLRef n)) (TLRef n)))))
\def
 \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (lt n d)).(eq_ind bool true (\lambda (b: bool).(eq T (TLRef (match b with [true \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef n))) (refl_equal T (TLRef n)) (blt n d) (sym_equal bool (blt n d) true (lt_blt d n H)))))).

theorem lift_lref_ge:
 \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((le d n) \to (eq T (lift h d (TLRef n)) (TLRef (plus n h))))))
\def
 \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (le d n)).(eq_ind bool false (\lambda (b: bool).(eq T (TLRef (match b with [true \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef (plus n h)))) (refl_equal T (TLRef (plus n h))) (blt n d) (sym_equal bool (blt n d) false (le_bge d n H)))))).

theorem lift_head:
 \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (THead k u t)) (THead k (lift h d u) (lift h (s k d) t)))))))
\def
 \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(refl_equal T (THead k (lift h d u) (lift h (s k d) t))))))).

theorem lift_bind:
 \forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (THead (Bind b) u t)) (THead (Bind b) (lift h d u) (lift h (S d) t)))))))
\def
 \lambda (b: B).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(refl_equal T (THead (Bind b) (lift h d u) (lift h (S d) t))))))).

theorem lift_flat:
 \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (THead (Flat f) u t)) (THead (Flat f) (lift h d u) (lift h d t)))))))
\def
 \lambda (f: F).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(refl_equal T (THead (Flat f) (lift h d u) (lift h d t))))))).

theorem lift_gen_sort:
 \forall (h: nat).(\forall (d: nat).(\forall (n: nat).(\forall (t: T).((eq T (TSort n) (lift h d t)) \to (eq T t (TSort n))))))
\def
 \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq T (TSort n) (lift h d t0)) \to (eq T t0 (TSort n)))) (\lambda (n0: nat).(\lambda (H: (eq T (TSort n) (lift h d (TSort n0)))).(sym_eq T (TSort n) (TSort n0) H))) (\lambda (n0: nat).(\lambda (H: (eq T (TSort n) (lift h d (TLRef n0)))).(lt_le_e n0 d (eq T (TLRef n0) (TSort n)) (\lambda (H0: (lt n0 d)).(let H1 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TSort n) t)) H (TLRef n0) (lift_lref_lt n0 h d H0)) in (let H2 \def (match H1 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (TLRef n0)) \to (eq T (TLRef n0) (TSort n))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (TSort n) (TLRef n0))).(let H2 \def (eq_ind T (TSort n) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef n0) H1) in (False_ind (eq T (TLRef n0) (TSort n)) H2)))]) in (H2 (refl_equal T (TLRef n0)))))) (\lambda (H0: (le d n0)).(let H1 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TSort n) t)) H (TLRef (plus n0 h)) (lift_lref_ge n0 h d H0)) in (let H2 \def (match H1 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (TLRef (plus n0 h))) \to (eq T (TLRef n0) (TSort n))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (TSort n) (TLRef (plus n0 h)))).(let H2 \def (eq_ind T (TSort n) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef (plus n0 h)) H1) in (False_ind (eq T (TLRef n0) (TSort n)) H2)))]) in (H2 (refl_equal T (TLRef (plus n0 h)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: (((eq T (TSort n) (lift h d t0)) \to (eq T t0 (TSort n))))).(\lambda (t1: T).(\lambda (_: (((eq T (TSort n) (lift h d t1)) \to (eq T t1 (TSort n))))).(\lambda (H1: (eq T (TSort n) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t: T).(eq T (TSort n) t)) H1 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def (match H2 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (THead k (lift h d t0) (lift h (s k d) t1))) \to (eq T (THead k t0 t1) (TSort n))))) with [refl_equal \Rightarrow (\lambda (H2: (eq T (TSort n) (THead k (lift h d t0) (lift h (s k d) t1)))).(let H3 \def (eq_ind T (TSort n) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead k (lift h d t0) (lift h (s k d) t1)) H2) in (False_ind (eq T (THead k t0 t1) (TSort n)) H3)))]) in (H3 (refl_equal T (THead k (lift h d t0) (lift h (s k d) t1)))))))))))) t)))).

theorem lift_gen_lref:
 \forall (t: T).(\forall (d: nat).(\forall (h: nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t)) \to (or (land (lt i d) (eq T t (TLRef i))) (land (le (plus d h) i) (eq T t (TLRef (minus i h)))))))))
\def
 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(\forall (h: nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t0)) \to (or (land (lt i d) (eq T t0 (TLRef i))) (land (le (plus d h) i) (eq T t0 (TLRef (minus i h)))))))))) (\lambda (n: nat).(\lambda (d: nat).(\lambda (h: nat).(\lambda (i: nat).(\lambda (H: (eq T (TLRef i) (lift h d (TSort n)))).(let H0 \def (eq_ind T (lift h d (TSort n)) (\lambda (t: T).(eq T (TLRef i) t)) H (TSort n) (lift_sort n h d)) in (let H1 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n) H0) in (False_ind (or (land (lt i d) (eq T (TSort n) (TLRef i))) (land (le (plus d h) i) (eq T (TSort n) (TLRef (minus i h))))) H1)))))))) (\lambda (n: nat).(\lambda (d: nat).(\lambda (h: nat).(\lambda (i: nat).(\lambda (H: (eq T (TLRef i) (lift h d (TLRef n)))).(lt_le_e n d (or (land (lt i d) (eq T (TLRef n) (TLRef i))) (land (le (plus d h) i) (eq T (TLRef n) (TLRef (minus i h))))) (\lambda (H0: (lt n d)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t: T).(eq T (TLRef i) t)) H (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (f_equal T nat (\lambda (e: T).(match e return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef n) H1) in (eq_ind_r nat n (\lambda (n0: nat).(or (land (lt n0 d) (eq T (TLRef n) (TLRef n0))) (land (le (plus d h) n0) (eq T (TLRef n) (TLRef (minus n0 h)))))) (or_introl (land (lt n d) (eq T (TLRef n) (TLRef n))) (land (le (plus d h) n) (eq T (TLRef n) (TLRef (minus n h)))) (conj (lt n d) (eq T (TLRef n) (TLRef n)) H0 (refl_equal T (TLRef n)))) i H2)))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t: T).(eq T (TLRef i) t)) H (TLRef (plus n h)) (lift_lref_ge n h d H0)) in (let H2 \def (f_equal T nat (\lambda (e: T).(match e return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef (plus n h)) H1) in (eq_ind_r nat (plus n h) (\lambda (n0: nat).(or (land (lt n0 d) (eq T (TLRef n) (TLRef n0))) (land (le (plus d h) n0) (eq T (TLRef n) (TLRef (minus n0 h)))))) (eq_ind_r nat n (\lambda (n0: nat).(or (land (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))) (land (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n0))))) (or_intror (land (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))) (land (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n))) (conj (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n)) (plus_le_compat d n h h H0 (le_n h)) (refl_equal T (TLRef n)))) (minus (plus n h) h) (minus_plus_r n h)) i H2)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: ((\forall (d: nat).(\forall (h: nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t0)) \to (or (land (lt i d) (eq T t0 (TLRef i))) (land (le (plus d h) i) (eq T t0 (TLRef (minus i h))))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (d: nat).(\forall (h: nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t1)) \to (or (land (lt i d) (eq T t1 (TLRef i))) (land (le (plus d h) i) (eq T t1 (TLRef (minus i h))))))))))).(\lambda (d: nat).(\lambda (h: nat).(\lambda (i: nat).(\lambda (H1: (eq T (TLRef i) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t: T).(eq T (TLRef i) t)) H1 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k (lift h d t0) (lift h (s k d) t1)) H2) in (False_ind (or (land (lt i d) (eq T (THead k t0 t1) (TLRef i))) (land (le (plus d h) i) (eq T (THead k t0 t1) (TLRef (minus i h))))) H3)))))))))))) t).

theorem lift_gen_lref_lt:
 \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((lt n d) \to (\forall (t: T).((eq T (TLRef n) (lift h d t)) \to (eq T t (TLRef n)))))))
\def
 \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (H: (lt n d)).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq T (TLRef n) (lift h d t0)) \to (eq T t0 (TLRef n)))) (\lambda (n0: nat).(\lambda (H0: (eq T (TLRef n) (lift h d (TSort n0)))).(sym_eq T (TLRef n) (TSort n0) H0))) (\lambda (n0: nat).(\lambda (H0: (eq T (TLRef n) (lift h d (TLRef n0)))).(lt_le_e n0 d (eq T (TLRef n0) (TLRef n)) (\lambda (H1: (lt n0 d)).(let H2 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef n) t)) H0 (TLRef n0) (lift_lref_lt n0 h d H1)) in (sym_eq T (TLRef n) (TLRef n0) H2))) (\lambda (H1: (le d n0)).(let H2 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef n) t)) H0 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H1)) in (let H3 \def (match H2 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (TLRef (plus n0 h))) \to (eq T (TLRef n0) (TLRef n))))) with [refl_equal \Rightarrow (\lambda (H2: (eq T (TLRef n) (TLRef (plus n0 h)))).(let H3 \def (f_equal T nat (\lambda (e: T).(match e return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef (plus n0 h)) H2) in (eq_ind nat (plus n0 h) (\lambda (n: nat).(eq T (TLRef n0) (TLRef n))) (let H0 \def (eq_ind nat n (\lambda (n: nat).(lt n d)) H (plus n0 h) H3) in (le_false d n0 (eq T (TLRef n0) (TLRef (plus n0 h))) H1 (lt_le_S n0 d (le_lt_trans n0 (plus n0 h) d (le_plus_l n0 h) H0)))) n (sym_eq nat n (plus n0 h) H3))))]) in (H3 (refl_equal T (TLRef (plus n0 h)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: (((eq T (TLRef n) (lift h d t0)) \to (eq T t0 (TLRef n))))).(\lambda (t1: T).(\lambda (_: (((eq T (TLRef n) (lift h d t1)) \to (eq T t1 (TLRef n))))).(\lambda (H2: (eq T (TLRef n) (lift h d (THead k t0 t1)))).(let H3 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t: T).(eq T (TLRef n) t)) H2 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H4 \def (match H3 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (THead k (lift h d t0) (lift h (s k d) t1))) \to (eq T (THead k t0 t1) (TLRef n))))) with [refl_equal \Rightarrow (\lambda (H3: (eq T (TLRef n) (THead k (lift h d t0) (lift h (s k d) t1)))).(let H4 \def (eq_ind T (TLRef n) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k (lift h d t0) (lift h (s k d) t1)) H3) in (False_ind (eq T (THead k t0 t1) (TLRef n)) H4)))]) in (H4 (refl_equal T (THead k (lift h d t0) (lift h (s k d) t1)))))))))))) t))))).

theorem lift_gen_lref_false:
 \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to ((lt n (plus d h)) \to (\forall (t: T).((eq T (TLRef n) (lift h d t)) \to (\forall (P: Prop).P)))))))
\def
 \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (H: (le d n)).(\lambda (H0: (lt n (plus d h))).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq T (TLRef n) (lift h d t0)) \to (\forall (P: Prop).P))) (\lambda (n0: nat).(\lambda (H1: (eq T (TLRef n) (lift h d (TSort n0)))).(\lambda (P: Prop).(let H2 \def (match H1 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (lift h d (TSort n0))) \to P))) with [refl_equal \Rightarrow (\lambda (H2: (eq T (TLRef n) (lift h d (TSort n0)))).(let H3 \def (eq_ind T (TLRef n) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (lift h d (TSort n0)) H2) in (False_ind P H3)))]) in (H2 (refl_equal T (lift h d (TSort n0)))))))) (\lambda (n0: nat).(\lambda (H1: (eq T (TLRef n) (lift h d (TLRef n0)))).(\lambda (P: Prop).(lt_le_e n0 d P (\lambda (H2: (lt n0 d)).(let H3 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef n) t)) H1 (TLRef n0) (lift_lref_lt n0 h d H2)) in (let H4 \def (match H3 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (TLRef n0)) \to P))) with [refl_equal \Rightarrow (\lambda (H3: (eq T (TLRef n) (TLRef n0))).(let H4 \def (f_equal T nat (\lambda (e: T).(match e return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef n0) H3) in (eq_ind nat n0 (\lambda (_: nat).P) (let H1 \def (eq_ind_r nat n0 (\lambda (n: nat).(lt n d)) H2 n H4) in (le_false d n P H H1)) n (sym_eq nat n n0 H4))))]) in (H4 (refl_equal T (TLRef n0)))))) (\lambda (H2: (le d n0)).(let H3 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef n) t)) H1 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H2)) in (let H4 \def (match H3 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (TLRef (plus n0 h))) \to P))) with [refl_equal \Rightarrow (\lambda (H3: (eq T (TLRef n) (TLRef (plus n0 h)))).(let H4 \def (f_equal T nat (\lambda (e: T).(match e return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef (plus n0 h)) H3) in (eq_ind nat (plus n0 h) (\lambda (_: nat).P) (let H1 \def (eq_ind nat n (\lambda (n: nat).(lt n (plus d h))) H0 (plus n0 h) H4) in (le_false d n0 P H2 (lt_le_S n0 d (simpl_lt_plus_r h n0 d H1)))) n (sym_eq nat n (plus n0 h) H4))))]) in (H4 (refl_equal T (TLRef (plus n0 h))))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: (((eq T (TLRef n) (lift h d t0)) \to (\forall (P: Prop).P)))).(\lambda (t1: T).(\lambda (_: (((eq T (TLRef n) (lift h d t1)) \to (\forall (P: Prop).P)))).(\lambda (H3: (eq T (TLRef n) (lift h d (THead k t0 t1)))).(\lambda (P: Prop).(let H4 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t: T).(eq T (TLRef n) t)) H3 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H5 \def (match H4 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (THead k (lift h d t0) (lift h (s k d) t1))) \to P))) with [refl_equal \Rightarrow (\lambda (H4: (eq T (TLRef n) (THead k (lift h d t0) (lift h (s k d) t1)))).(let H5 \def (eq_ind T (TLRef n) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k (lift h d t0) (lift h (s k d) t1)) H4) in (False_ind P H5)))]) in (H5 (refl_equal T (THead k (lift h d t0) (lift h (s k d) t1))))))))))))) t)))))).

theorem lift_gen_lref_ge:
 \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to (\forall (t: T).((eq T (TLRef (plus n h)) (lift h d t)) \to (eq T t (TLRef n)))))))
\def
 \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (H: (le d n)).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq T (TLRef (plus n h)) (lift h d t0)) \to (eq T t0 (TLRef n)))) (\lambda (n0: nat).(\lambda (H0: (eq T (TLRef (plus n h)) (lift h d (TSort n0)))).(let H1 \def (match H0 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (lift h d (TSort n0))) \to (eq T (TSort n0) (TLRef n))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (TLRef (plus n h)) (lift h d (TSort n0)))).(let H2 \def (eq_ind T (TLRef (plus n h)) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (lift h d (TSort n0)) H1) in (False_ind (eq T (TSort n0) (TLRef n)) H2)))]) in (H1 (refl_equal T (lift h d (TSort n0))))))) (\lambda (n0: nat).(\lambda (H0: (eq T (TLRef (plus n h)) (lift h d (TLRef n0)))).(lt_le_e n0 d (eq T (TLRef n0) (TLRef n)) (\lambda (H1: (lt n0 d)).(let H2 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef (plus n h)) t)) H0 (TLRef n0) (lift_lref_lt n0 h d H1)) in (let H3 \def (match H2 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (TLRef n0)) \to (eq T (TLRef n0) (TLRef n))))) with [refl_equal \Rightarrow (\lambda (H2: (eq T (TLRef (plus n h)) (TLRef n0))).(let H3 \def (f_equal T nat (\lambda (e: T).(match e return (\lambda (_: T).nat) with [(TSort _) \Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h) | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h)])) (TLRef (plus n h)) (TLRef n0) H2) in (eq_ind nat (plus n h) (\lambda (n0: nat).(eq T (TLRef n0) (TLRef n))) (let H0 \def (eq_ind_r nat n0 (\lambda (n: nat).(lt n d)) H1 (plus n h) H3) in (le_false d n (eq T (TLRef (plus n h)) (TLRef n)) H (lt_le_S n d (le_lt_trans n (plus n h) d (le_plus_l n h) H0)))) n0 H3)))]) in (H3 (refl_equal T (TLRef n0)))))) (\lambda (H1: (le d n0)).(let H2 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef (plus n h)) t)) H0 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H1)) in (let H3 \def (match H2 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (TLRef (plus n0 h))) \to (eq T (TLRef n0) (TLRef n))))) with [refl_equal \Rightarrow (\lambda (H2: (eq T (TLRef (plus n h)) (TLRef (plus n0 h)))).(let H3 \def (f_equal T nat (\lambda (e: T).(match e return (\lambda (_: T).nat) with [(TSort _) \Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h) | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h)])) (TLRef (plus n h)) (TLRef (plus n0 h)) H2) in (eq_ind nat (plus n h) (\lambda (_: nat).(eq T (TLRef n0) (TLRef n))) (f_equal nat T TLRef n0 n (simpl_plus_r h n0 n (sym_eq nat (plus n h) (plus n0 h) H3))) (plus n0 h) H3)))]) in (H3 (refl_equal T (TLRef (plus n0 h)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: (((eq T (TLRef (plus n h)) (lift h d t0)) \to (eq T t0 (TLRef n))))).(\lambda (t1: T).(\lambda (_: (((eq T (TLRef (plus n h)) (lift h d t1)) \to (eq T t1 (TLRef n))))).(\lambda (H2: (eq T (TLRef (plus n h)) (lift h d (THead k t0 t1)))).(let H3 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t: T).(eq T (TLRef (plus n h)) t)) H2 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H4 \def (match H3 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (THead k (lift h d t0) (lift h (s k d) t1))) \to (eq T (THead k t0 t1) (TLRef n))))) with [refl_equal \Rightarrow (\lambda (H3: (eq T (TLRef (plus n h)) (THead k (lift h d t0) (lift h (s k d) t1)))).(let H4 \def (eq_ind T (TLRef (plus n h)) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k (lift h d t0) (lift h (s k d) t1)) H3) in (False_ind (eq T (THead k t0 t1) (TLRef n)) H4)))]) in (H4 (refl_equal T (THead k (lift h d t0) (lift h (s k d) t1)))))))))))) t))))).

theorem lift_gen_head:
 \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k u t) (lift h d x)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T x (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))))))
\def
 \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (x: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k u t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead k u t) (lift h d (TSort n)))).(let H0 \def (match H return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (lift h d (TSort n))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda (H0: (eq T (THead k u t) (lift h d (TSort n)))).(let H1 \def (eq_ind T (THead k u t) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (lift h d (TSort n)) H0) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z))))) H1)))]) in (H0 (refl_equal T (lift h d (TSort n))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead k u t) (lift h d (TLRef n)))).(lt_le_e n d (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z))))) (\lambda (H0: (lt n d)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead k u t) t0)) H (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (THead k u t) (TLRef n))).(let H2 \def (eq_ind T (THead k u t) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z))))) H2)))]) in (H2 (refl_equal T (TLRef n)))))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead k u t) t0)) H (TLRef (plus n h)) (lift_lref_ge n h d H0)) in (let H2 \def (match H1 return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (THead k u t) (TLRef (plus n h)))).(let H2 \def (eq_ind T (THead k u t) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef (plus n h)) H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z))))) H2)))]) in (H2 (refl_equal T (TLRef (plus n h)))))))))))) (\lambda (k0: K).(\lambda (t0: T).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead k u t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead k u t) (lift h d t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t1 (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T (THead k u t) (lift h d (THead k0 t0 t1)))).(let H2 \def (eq_ind T (lift h d (THead k0 t0 t1)) (\lambda (t0: T).(eq T (THead k u t) t0)) H1 (THead k0 (lift h d t0) (lift h (s k0 d) t1)) (lift_head k0 t0 t1 h d)) in (let H3 \def (match H2 return (\lambda (t2: T).(\lambda (_: (eq ? ? t2)).((eq T t2 (THead k0 (lift h d t0) (lift h (s k0 d) t1))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda (H2: (eq T (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1)))).(let H3 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t) \Rightarrow t])) (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1)) H2) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t])) (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1)) H2) in ((let H5 \def (f_equal T K (\lambda (e: T).(match e return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1)) H2) in (eq_ind K k0 (\lambda (k: K).((eq T u (lift h d t0)) \to ((eq T t (lift h (s k0 d) t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))) (\lambda (H6: (eq T u (lift h d t0))).(eq_ind T (lift h d t0) (\lambda (t2: T).((eq T t (lift h (s k0 d) t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead k0 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T t2 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k0 d) z))))))) (\lambda (H7: (eq T t (lift h (s k0 d) t1))).(eq_ind T (lift h (s k0 d) t1) (\lambda (t: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead k0 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k0 d) z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead k0 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s k0 d) t1) (lift h (s k0 d) z)))) t0 t1 (refl_equal T (THead k0 t0 t1)) (refl_equal T (lift h d t0)) (refl_equal T (lift h (s k0 d) t1))) t (sym_eq T t (lift h (s k0 d) t1) H7))) u (sym_eq T u (lift h d t0) H6))) k (sym_eq K k k0 H5))) H4)) H3)))]) in (H3 (refl_equal T (THead k0 (lift h d t0) (lift h (s k0 d) t1)))))))))))))) x)))).

theorem lift_gen_bind:
 \forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead (Bind b) u t) (lift h d x)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))))))
\def
 \lambda (b: B).(\lambda (u: T).(\lambda (t: T).(\lambda (x: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead (Bind b) u t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Bind b) u t) (lift h d (TSort n)))).(let H0 \def (match H return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (lift h d (TSort n))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal \Rightarrow (\lambda (H0: (eq T (THead (Bind b) u t) (lift h d (TSort n)))).(let H1 \def (eq_ind T (THead (Bind b) u t) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (lift h d (TSort n)) H0) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))) H1)))]) in (H0 (refl_equal T (lift h d (TSort n))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Bind b) u t) (lift h d (TLRef n)))).(lt_le_e n d (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))) (\lambda (H0: (lt n d)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead (Bind b) u t) t0)) H (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (THead (Bind b) u t) (TLRef n))).(let H2 \def (eq_ind T (THead (Bind b) u t) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))) H2)))]) in (H2 (refl_equal T (TLRef n)))))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead (Bind b) u t) t0)) H (TLRef (plus n h)) (lift_lref_ge n h d H0)) in (let H2 \def (match H1 return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (THead (Bind b) u t) (TLRef (plus n h)))).(let H2 \def (eq_ind T (THead (Bind b) u t) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef (plus n h)) H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))) H2)))]) in (H2 (refl_equal T (TLRef (plus n h)))))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Bind b) u t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Bind b) u t) (lift h d t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t1 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T (THead (Bind b) u t) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t0: T).(eq T (THead (Bind b) u t) t0)) H1 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def (match H2 return (\lambda (t2: T).(\lambda (_: (eq ? ? t2)).((eq T t2 (THead k (lift h d t0) (lift h (s k d) t1))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k t0 t1) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal \Rightarrow (\lambda (H2: (eq T (THead (Bind b) u t) (THead k (lift h d t0) (lift h (s k d) t1)))).(let H3 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t) \Rightarrow t])) (THead (Bind b) u t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t])) (THead (Bind b) u t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let H5 \def (f_equal T K (\lambda (e: T).(match e return (\lambda (_: T).K) with [(TSort _) \Rightarrow (Bind b) | (TLRef _) \Rightarrow (Bind b) | (THead k _ _) \Rightarrow k])) (THead (Bind b) u t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in (eq_ind K (Bind b) (\lambda (k: K).((eq T u (lift h d t0)) \to ((eq T t (lift h (s k d) t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k t0 t1) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) (\lambda (H6: (eq T u (lift h d t0))).(eq_ind T (lift h d t0) (\lambda (t2: T).((eq T t (lift h (s (Bind b) d) t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Bind b) t0 t1) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T t2 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))))) (\lambda (H7: (eq T t (lift h (s (Bind b) d) t1))).(eq_ind T (lift h (s (Bind b) d) t1) (\lambda (t: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Bind b) t0 t1) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Bind b) t0 t1) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s (Bind b) d) t1) (lift h (S d) z)))) t0 t1 (refl_equal T (THead (Bind b) t0 t1)) (refl_equal T (lift h d t0)) (refl_equal T (lift h (S d) t1))) t (sym_eq T t (lift h (s (Bind b) d) t1) H7))) u (sym_eq T u (lift h d t0) H6))) k H5)) H4)) H3)))]) in (H3 (refl_equal T (THead k (lift h d t0) (lift h (s k d) t1)))))))))))))) x)))).

theorem lift_gen_flat:
 \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h d x)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))))))
\def
 \lambda (f: F).(\lambda (u: T).(\lambda (t: T).(\lambda (x: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Flat f) u t) (lift h d (TSort n)))).(let H0 \def (match H return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (lift h d (TSort n))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow (\lambda (H0: (eq T (THead (Flat f) u t) (lift h d (TSort n)))).(let H1 \def (eq_ind T (THead (Flat f) u t) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (lift h d (TSort n)) H0) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))) H1)))]) in (H0 (refl_equal T (lift h d (TSort n))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Flat f) u t) (lift h d (TLRef n)))).(lt_le_e n d (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))) (\lambda (H0: (lt n d)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead (Flat f) u t) t0)) H (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (THead (Flat f) u t) (TLRef n))).(let H2 \def (eq_ind T (THead (Flat f) u t) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))) H2)))]) in (H2 (refl_equal T (TLRef n)))))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead (Flat f) u t) t0)) H (TLRef (plus n h)) (lift_lref_ge n h d H0)) in (let H2 \def (match H1 return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (THead (Flat f) u t) (TLRef (plus n h)))).(let H2 \def (eq_ind T (THead (Flat f) u t) (\lambda (e: T).(match e return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef (plus n h)) H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))) H2)))]) in (H2 (refl_equal T (TLRef (plus n h)))))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h d t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t1 (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T (THead (Flat f) u t) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t0: T).(eq T (THead (Flat f) u t) t0)) H1 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def (match H2 return (\lambda (t2: T).(\lambda (_: (eq ? ? t2)).((eq T t2 (THead k (lift h d t0) (lift h (s k d) t1))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow (\lambda (H2: (eq T (THead (Flat f) u t) (THead k (lift h d t0) (lift h (s k d) t1)))).(let H3 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t) \Rightarrow t])) (THead (Flat f) u t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t])) (THead (Flat f) u t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let H5 \def (f_equal T K (\lambda (e: T).(match e return (\lambda (_: T).K) with [(TSort _) \Rightarrow (Flat f) | (TLRef _) \Rightarrow (Flat f) | (THead k _ _) \Rightarrow k])) (THead (Flat f) u t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in (eq_ind K (Flat f) (\lambda (k: K).((eq T u (lift h d t0)) \to ((eq T t (lift h (s k d) t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))) (\lambda (H6: (eq T u (lift h d t0))).(eq_ind T (lift h d t0) (\lambda (t2: T).((eq T t (lift h (s (Flat f) d) t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Flat f) t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T t2 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))))) (\lambda (H7: (eq T t (lift h (s (Flat f) d) t1))).(eq_ind T (lift h (s (Flat f) d) t1) (\lambda (t: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Flat f) t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Flat f) t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s (Flat f) d) t1) (lift h d z)))) t0 t1 (refl_equal T (THead (Flat f) t0 t1)) (refl_equal T (lift h d t0)) (refl_equal T (lift h d t1))) t (sym_eq T t (lift h (s (Flat f) d) t1) H7))) u (sym_eq T u (lift h d t0) H6))) k H5)) H4)) H3)))]) in (H3 (refl_equal T (THead k (lift h d t0) (lift h (s k d) t1)))))))))))))) x)))).

theorem thead_x_lift_y_y:
 \forall (k: K).(\forall (t: T).(\forall (v: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k v (lift h d t)) t) \to (\forall (P: Prop).P))))))
\def
 \lambda (k: K).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (v: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k v (lift h d t0)) t0) \to (\forall (P: Prop).P)))))) (\lambda (n: nat).(\lambda (v: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead k v (lift h d (TSort n))) (TSort n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead k v (lift h d (TSort n))) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H) in (False_ind P H0)))))))) (\lambda (n: nat).(\lambda (v: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead k v (lift h d (TLRef n))) (TLRef n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead k v (lift h d (TLRef n))) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H) in (False_ind P H0)))))))) (\lambda (k0: K).(\lambda (t0: T).(\lambda (_: ((\forall (v: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k v (lift h d t0)) t0) \to (\forall (P: Prop).P))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (v: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k v (lift h d t1)) t1) \to (\forall (P: Prop).P))))))).(\lambda (v: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e: T).(match e return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1) H1) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t _) \Rightarrow t])) (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead k0 ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0) \Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))]) in lref_map) (\lambda (x: nat).(plus x h)) d t0) ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0) \Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))]) in lref_map) (\lambda (x: nat).(plus x h)) (s k0 d) t1)) | (TLRef _) \Rightarrow (THead k0 ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0) \Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))]) in lref_map) (\lambda (x: nat).(plus x h)) d t0) ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0) \Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))]) in lref_map) (\lambda (x: nat).(plus x h)) (s k0 d) t1)) | (THead _ _ t) \Rightarrow t])) (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1) H1) in (\lambda (_: (eq T v t0)).(\lambda (H6: (eq K k k0)).(let H7 \def (eq_ind K k (\lambda (k: K).(\forall (v: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k v (lift h d t1)) t1) \to (\forall (P: Prop).P)))))) H0 k0 H6) in (let H8 \def (eq_ind T (lift h d (THead k0 t0 t1)) (\lambda (t: T).(eq T t t1)) H4 (THead k0 (lift h d t0) (lift h (s k0 d) t1)) (lift_head k0 t0 t1 h d)) in (H7 (lift h d t0) h (s k0 d) H8 P)))))) H3)) H2)))))))))))) t)).

theorem lift_r:
 \forall (t: T).(\forall (d: nat).(eq T (lift O d t) t))
\def
 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(eq T (lift O d t0) t0))) (\lambda (n: nat).(\lambda (_: nat).(refl_equal T (TSort n)))) (\lambda (n: nat).(\lambda (d: nat).(lt_le_e n d (eq T (lift O d (TLRef n)) (TLRef n)) (\lambda (H: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 (TLRef n))) (refl_equal T (TLRef n)) (lift O d (TLRef n)) (lift_lref_lt n O d H))) (\lambda (H: (le d n)).(eq_ind_r T (TLRef (plus n O)) (\lambda (t0: T).(eq T t0 (TLRef n))) (f_equal nat T TLRef (plus n O) n (sym_eq nat n (plus n O) (plus_n_O n))) (lift O d (TLRef n)) (lift_lref_ge n O d H)))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (d: nat).(eq T (lift O d t0) t0)))).(\lambda (t1: T).(\lambda (H0: ((\forall (d: nat).(eq T (lift O d t1) t1)))).(\lambda (d: nat).(eq_ind_r T (THead k (lift O d t0) (lift O (s k d) t1)) (\lambda (t2: T).(eq T t2 (THead k t0 t1))) (sym_equal T (THead k t0 t1) (THead k (lift O d t0) (lift O (s k d) t1)) (sym_equal T (THead k (lift O d t0) (lift O (s k d) t1)) (THead k t0 t1) (sym_equal T (THead k t0 t1) (THead k (lift O d t0) (lift O (s k d) t1)) (f_equal3 K T T T THead k k t0 (lift O d t0) t1 (lift O (s k d) t1) (refl_equal K k) (sym_eq T (lift O d t0) t0 (H d)) (sym_eq T (lift O (s k d) t1) t1 (H0 (s k d))))))) (lift O d (THead k t0 t1)) (lift_head k t0 t1 O d)))))))) t).

theorem lift_lref_gt:
 \forall (d: nat).(\forall (n: nat).((lt d n) \to (eq T (lift (S O) d (TLRef (pred n))) (TLRef n))))
\def
 \lambda (d: nat).(\lambda (n: nat).(\lambda (H: (lt d n)).(eq_ind_r T (TLRef (plus (pred n) (S O))) (\lambda (t: T).(eq T t (TLRef n))) (eq_ind nat (plus (S O) (pred n)) (\lambda (n0: nat).(eq T (TLRef n0) (TLRef n))) (eq_ind nat n (\lambda (n0: nat).(eq T (TLRef n0) (TLRef n))) (refl_equal T (TLRef n)) (S (pred n)) (S_pred n d H)) (plus (pred n) (S O)) (plus_comm (S O) (pred n))) (lift (S O) d (TLRef (pred n))) (lift_lref_ge (pred n) (S O) d (le_S_n d (pred n) (eq_ind nat n (\lambda (n0: nat).(le (S d) n0)) H (S (pred n)) (S_pred n d H))))))).

theorem lift_inj:
 \forall (x: T).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).((eq T (lift h d x) (lift h d t)) \to (eq T x t)))))
\def
 \lambda (x: T).(T_ind (\lambda (t: T).(\forall (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (lift h d t) (lift h d t0)) \to (eq T t t0)))))) (\lambda (n: nat).(\lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (lift h d (TSort n)) (lift h d t))).(let H0 \def (eq_ind T (lift h d (TSort n)) (\lambda (t0: T).(eq T t0 (lift h d t))) H (TSort n) (lift_sort n h d)) in (sym_eq T t (TSort n) (lift_gen_sort h d n t H0)))))))) (\lambda (n: nat).(\lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (lift h d (TLRef n)) (lift h d t))).(lt_le_e n d (eq T (TLRef n) t) (\lambda (H0: (lt n d)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T t0 (lift h d t))) H (TLRef n) (lift_lref_lt n h d H0)) in (sym_eq T t (TLRef n) (lift_gen_lref_lt h d n (lt_le_trans n d d H0 (le_n d)) t H1)))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T t0 (lift h d t))) H (TLRef (plus n h)) (lift_lref_ge n h d H0)) in (sym_eq T t (TLRef n) (lift_gen_lref_ge h d n H0 t H1)))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t: T).(((\forall (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (lift h d t) (lift h d t0)) \to (eq T t t0)))))) \to (\forall (t0: T).(((\forall (t: T).(\forall (h: nat).(\forall (d: nat).((eq T (lift h d t0) (lift h d t)) \to (eq T t0 t)))))) \to (\forall (t1: T).(\forall (h: nat).(\forall (d: nat).((eq T (lift h d (THead k0 t t0)) (lift h d t1)) \to (eq T (THead k0 t t0) t1)))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H: ((\forall (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (lift h d t) (lift h d t0)) \to (eq T t t0))))))).(\lambda (t0: T).(\lambda (H0: ((\forall (t: T).(\forall (h: nat).(\forall (d: nat).((eq T (lift h d t0) (lift h d t)) \to (eq T t0 t))))))).(\lambda (t1: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T (lift h d (THead (Bind b) t t0)) (lift h d t1))).(let H2 \def (eq_ind T (lift h d (THead (Bind b) t t0)) (\lambda (t: T).(eq T t (lift h d t1))) H1 (THead (Bind b) (lift h d t) (lift h (S d) t0)) (lift_bind b t t0 h d)) in (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T t1 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (S d) t0) (lift h (S d) z)))) (eq T (THead (Bind b) t t0) t1) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H3: (eq T t1 (THead (Bind b) x0 x1))).(\lambda (H4: (eq T (lift h d t) (lift h d x0))).(\lambda (H5: (eq T (lift h (S d) t0) (lift h (S d) x1))).(eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t2: T).(eq T (THead (Bind b) t t0) t2)) (sym_equal T (THead (Bind b) x0 x1) (THead (Bind b) t t0) (sym_equal T (THead (Bind b) t t0) (THead (Bind b) x0 x1) (sym_equal T (THead (Bind b) x0 x1) (THead (Bind b) t t0) (f_equal3 K T T T THead (Bind b) (Bind b) x0 t x1 t0 (refl_equal K (Bind b)) (sym_eq T t x0 (H x0 h d H4)) (sym_eq T t0 x1 (H0 x1 h (S d) H5)))))) t1 H3)))))) (lift_gen_bind b (lift h d t) (lift h (S d) t0) t1 h d H2)))))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda (H: ((\forall (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (lift h d t) (lift h d t0)) \to (eq T t t0))))))).(\lambda (t0: T).(\lambda (H0: ((\forall (t: T).(\forall (h: nat).(\forall (d: nat).((eq T (lift h d t0) (lift h d t)) \to (eq T t0 t))))))).(\lambda (t1: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T (lift h d (THead (Flat f) t t0)) (lift h d t1))).(let H2 \def (eq_ind T (lift h d (THead (Flat f) t t0)) (\lambda (t: T).(eq T t (lift h d t1))) H1 (THead (Flat f) (lift h d t) (lift h d t0)) (lift_flat f t t0 h d)) in (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T t1 (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h d t0) (lift h d z)))) (eq T (THead (Flat f) t t0) t1) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H3: (eq T t1 (THead (Flat f) x0 x1))).(\lambda (H4: (eq T (lift h d t) (lift h d x0))).(\lambda (H5: (eq T (lift h d t0) (lift h d x1))).(eq_ind_r T (THead (Flat f) x0 x1) (\lambda (t2: T).(eq T (THead (Flat f) t t0) t2)) (sym_equal T (THead (Flat f) x0 x1) (THead (Flat f) t t0) (sym_equal T (THead (Flat f) t t0) (THead (Flat f) x0 x1) (sym_equal T (THead (Flat f) x0 x1) (THead (Flat f) t t0) (f_equal3 K T T T THead (Flat f) (Flat f) x0 t x1 t0 (refl_equal K (Flat f)) (sym_eq T t x0 (H x0 h d H4)) (sym_eq T t0 x1 (H0 x1 h d H5)))))) t1 H3)))))) (lift_gen_flat f (lift h d t) (lift h d t0) t1 h d H2)))))))))))) k)) x).

theorem lift_gen_lift:
 \forall (t1: T).(\forall (x: T).(\forall (h1: nat).(\forall (h2: nat).(\forall (d1: nat).(\forall (d2: nat).((le d1 d2) \to ((eq T (lift h1 d1 t1) (lift h2 (plus d2 h1) x)) \to (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T t1 (lift h2 d2 t2)))))))))))
\def
 \lambda (t1: T).(T_ind (\lambda (t: T).(\forall (x: T).(\forall (h1: nat).(\forall (h2: nat).(\forall (d1: nat).(\forall (d2: nat).((le d1 d2) \to ((eq T (lift h1 d1 t) (lift h2 (plus d2 h1) x)) \to (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T t (lift h2 d2 t2)))))))))))) (\lambda (n: nat).(\lambda (x: T).(\lambda (h1: nat).(\lambda (h2: nat).(\lambda (d1: nat).(\lambda (d2: nat).(\lambda (_: (le d1 d2)).(\lambda (H0: (eq T (lift h1 d1 (TSort n)) (lift h2 (plus d2 h1) x))).(let H1 \def (eq_ind T (lift h1 d1 (TSort n)) (\lambda (t: T).(eq T t (lift h2 (plus d2 h1) x))) H0 (TSort n) (lift_sort n h1 d1)) in (eq_ind_r T (TSort n) (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TSort n) (lift h2 d2 t2))))) (ex_intro2 T (\lambda (t2: T).(eq T (TSort n) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TSort n) (lift h2 d2 t2))) (TSort n) (eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal T (TSort n)) (lift h1 d1 (TSort n)) (lift_sort n h1 d1)) (eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal T (TSort n)) (lift h2 d2 (TSort n)) (lift_sort n h2 d2))) x (lift_gen_sort h2 (plus d2 h1) n x H1))))))))))) (\lambda (n: nat).(\lambda (x: T).(\lambda (h1: nat).(\lambda (h2: nat).(\lambda (d1: nat).(\lambda (d2: nat).(\lambda (H: (le d1 d2)).(\lambda (H0: (eq T (lift h1 d1 (TLRef n)) (lift h2 (plus d2 h1) x))).(lt_le_e n d1 (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2)))) (\lambda (H1: (lt n d1)).(let H2 \def (eq_ind T (lift h1 d1 (TLRef n)) (\lambda (t: T).(eq T t (lift h2 (plus d2 h1) x))) H0 (TLRef n) (lift_lref_lt n h1 d1 H1)) in (eq_ind_r T (TLRef n) (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))))) (ex_intro2 T (\lambda (t2: T).(eq T (TLRef n) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))) (TLRef n) (eq_ind_r T (TLRef n) (\lambda (t: T).(eq T (TLRef n) t)) (refl_equal T (TLRef n)) (lift h1 d1 (TLRef n)) (lift_lref_lt n h1 d1 H1)) (eq_ind_r T (TLRef n) (\lambda (t: T).(eq T (TLRef n) t)) (refl_equal T (TLRef n)) (lift h2 d2 (TLRef n)) (lift_lref_lt n h2 d2 (lt_le_trans n d1 d2 H1 H)))) x (lift_gen_lref_lt h2 (plus d2 h1) n (lt_le_trans n d1 (plus d2 h1) H1 (le_plus_trans d1 d2 h1 H)) x H2)))) (\lambda (H1: (le d1 n)).(let H2 \def (eq_ind T (lift h1 d1 (TLRef n)) (\lambda (t: T).(eq T t (lift h2 (plus d2 h1) x))) H0 (TLRef (plus n h1)) (lift_lref_ge n h1 d1 H1)) in (lt_le_e n d2 (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2)))) (\lambda (H3: (lt n d2)).(eq_ind_r T (TLRef (plus n h1)) (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))))) (ex_intro2 T (\lambda (t2: T).(eq T (TLRef (plus n h1)) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))) (TLRef n) (eq_ind_r T (TLRef (plus n h1)) (\lambda (t: T).(eq T (TLRef (plus n h1)) t)) (refl_equal T (TLRef (plus n h1))) (lift h1 d1 (TLRef n)) (lift_lref_ge n h1 d1 H1)) (eq_ind_r T (TLRef n) (\lambda (t: T).(eq T (TLRef n) t)) (refl_equal T (TLRef n)) (lift h2 d2 (TLRef n)) (lift_lref_lt n h2 d2 H3))) x (lift_gen_lref_lt h2 (plus d2 h1) (plus n h1) (plus_lt_compat_r n d2 h1 H3) x H2))) (\lambda (H3: (le d2 n)).(lt_le_e n (plus d2 h2) (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2)))) (\lambda (H4: (lt n (plus d2 h2))).(lift_gen_lref_false h2 (plus d2 h1) (plus n h1) (le_S_n (plus d2 h1) (plus n h1) (lt_le_S (plus d2 h1) (S (plus n h1)) (le_lt_n_Sm (plus d2 h1) (plus n h1) (plus_le_compat d2 n h1 h1 H3 (le_n h1))))) (eq_ind_r nat (plus (plus d2 h2) h1) (\lambda (n0: nat).(lt (plus n h1) n0)) (lt_le_S (plus n h1) (plus (plus d2 h2) h1) (plus_lt_compat_r n (plus d2 h2) h1 H4)) (plus (plus d2 h1) h2) (plus_permute_2_in_3 d2 h1 h2)) x H2 (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2)))))) (\lambda (H4: (le (plus d2 h2) n)).(let H5 \def (eq_ind nat (plus n h1) (\lambda (n: nat).(eq T (TLRef n) (lift h2 (plus d2 h1) x))) H2 (plus (minus (plus n h1) h2) h2) (le_plus_minus_sym h2 (plus n h1) (le_plus_trans h2 n h1 (le_trans_plus_r d2 h2 n H4)))) in (eq_ind_r T (TLRef (minus (plus n h1) h2)) (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))))) (ex_intro2 T (\lambda (t2: T).(eq T (TLRef (minus (plus n h1) h2)) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))) (TLRef (minus n h2)) (eq_ind_r nat (plus (minus n h2) h1) (\lambda (n0: nat).(eq T (TLRef n0) (lift h1 d1 (TLRef (minus n h2))))) (eq_ind_r T (TLRef (plus (minus n h2) h1)) (\lambda (t: T).(eq T (TLRef (plus (minus n h2) h1)) t)) (refl_equal T (TLRef (plus (minus n h2) h1))) (lift h1 d1 (TLRef (minus n h2))) (lift_lref_ge (minus n h2) h1 d1 (le_trans d1 d2 (minus n h2) H (le_minus d2 n h2 H4)))) (minus (plus n h1) h2) (le_minus_plus h2 n (le_trans_plus_r d2 h2 n H4) h1)) (eq_ind_r nat (plus (minus n h2) h2) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2 d2 (TLRef (minus n0 h2))))) (eq_ind_r T (TLRef (plus (minus (plus (minus n h2) h2) h2) h2)) (\lambda (t: T).(eq T (TLRef (plus (minus n h2) h2)) t)) (f_equal nat T TLRef (plus (minus n h2) h2) (plus (minus (plus (minus n h2) h2) h2) h2) (f_equal2 nat nat nat plus (minus n h2) (minus (plus (minus n h2) h2) h2) h2 h2 (sym_eq nat (minus (plus (minus n h2) h2) h2) (minus n h2) (minus_plus_r (minus n h2) h2)) (refl_equal nat h2))) (lift h2 d2 (TLRef (minus (plus (minus n h2) h2) h2))) (lift_lref_ge (minus (plus (minus n h2) h2) h2) h2 d2 (le_minus d2 (plus (minus n h2) h2) h2 (plus_le_compat d2 (minus n h2) h2 h2 (le_minus d2 n h2 H4) (le_n h2))))) n (le_plus_minus_sym h2 n (le_trans_plus_r d2 h2 n H4)))) x (lift_gen_lref_ge h2 (plus d2 h1) (minus (plus n h1) h2) (arith0 h2 d2 n H4 h1) x H5)))))))))))))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (x: T).(\forall (h1: nat).(\forall (h2: nat).(\forall (d1: nat).(\forall (d2: nat).((le d1 d2) \to ((eq T (lift h1 d1 t) (lift h2 (plus d2 h1) x)) \to (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T t (lift h2 d2 t2))))))))))))).(\lambda (t0: T).(\lambda (H0: ((\forall (x: T).(\forall (h1: nat).(\forall (h2: nat).(\forall (d1: nat).(\forall (d2: nat).((le d1 d2) \to ((eq T (lift h1 d1 t0) (lift h2 (plus d2 h1) x)) \to (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T t0 (lift h2 d2 t2))))))))))))).(\lambda (x: T).(\lambda (h1: nat).(\lambda (h2: nat).(\lambda (d1: nat).(\lambda (d2: nat).(\lambda (H1: (le d1 d2)).(\lambda (H2: (eq T (lift h1 d1 (THead k t t0)) (lift h2 (plus d2 h1) x))).(K_ind (\lambda (k0: K).((eq T (lift h1 d1 (THead k0 t t0)) (lift h2 (plus d2 h1) x)) \to (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (THead k0 t t0) (lift h2 d2 t2)))))) (\lambda (b: B).(\lambda (H3: (eq T (lift h1 d1 (THead (Bind b) t t0)) (lift h2 (plus d2 h1) x))).(let H4 \def (eq_ind T (lift h1 d1 (THead (Bind b) t t0)) (\lambda (t: T).(eq T t (lift h2 (plus d2 h1) x))) H3 (THead (Bind b) (lift h1 d1 t) (lift h1 (S d1) t0)) (lift_bind b t t0 h1 d1)) in (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h1 d1 t) (lift h2 (plus d2 h1) y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h1 (S d1) t0) (lift h2 (S (plus d2 h1)) z)))) (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (THead (Bind b) t t0) (lift h2 d2 t2)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T x (THead (Bind b) x0 x1))).(\lambda (H6: (eq T (lift h1 d1 t) (lift h2 (plus d2 h1) x0))).(\lambda (H7: (eq T (lift h1 (S d1) t0) (lift h2 (S (plus d2 h1)) x1))).(eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T t2 (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Bind b) t t0) (lift h2 d2 t3))))) (ex2_ind T (\lambda (t2: T).(eq T x0 (lift h1 d1 t2))) (\lambda (t2: T).(eq T t (lift h2 d2 t2))) (ex2 T (\lambda (t2: T).(eq T (THead (Bind b) x0 x1) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (THead (Bind b) t t0) (lift h2 d2 t2)))) (\lambda (x2: T).(\lambda (H8: (eq T x0 (lift h1 d1 x2))).(\lambda (H9: (eq T t (lift h2 d2 x2))).(eq_ind_r T (lift h1 d1 x2) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T (THead (Bind b) t2 x1) (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Bind b) t t0) (lift h2 d2 t3))))) (eq_ind_r T (lift h2 d2 x2) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T (THead (Bind b) (lift h1 d1 x2) x1) (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Bind b) t2 t0) (lift h2 d2 t3))))) (let H10 \def (refl_equal nat (plus (S d2) h1)) in (let H11 \def (eq_ind nat (S (plus d2 h1)) (\lambda (n: nat).(eq T (lift h1 (S d1) t0) (lift h2 n x1))) H7 (plus (S d2) h1) H10) in (ex2_ind T (\lambda (t2: T).(eq T x1 (lift h1 (S d1) t2))) (\lambda (t2: T).(eq T t0 (lift h2 (S d2) t2))) (ex2 T (\lambda (t2: T).(eq T (THead (Bind b) (lift h1 d1 x2) x1) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (THead (Bind b) (lift h2 d2 x2) t0) (lift h2 d2 t2)))) (\lambda (x3: T).(\lambda (H12: (eq T x1 (lift h1 (S d1) x3))).(\lambda (H13: (eq T t0 (lift h2 (S d2) x3))).(eq_ind_r T (lift h1 (S d1) x3) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T (THead (Bind b) (lift h1 d1 x2) t2) (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Bind b) (lift h2 d2 x2) t0) (lift h2 d2 t3))))) (eq_ind_r T (lift h2 (S d2) x3) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T (THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)) (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Bind b) (lift h2 d2 x2) t2) (lift h2 d2 t3))))) (ex_intro2 T (\lambda (t2: T).(eq T (THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (THead (Bind b) (lift h2 d2 x2) (lift h2 (S d2) x3)) (lift h2 d2 t2))) (THead (Bind b) x2 x3) (eq_ind_r T (THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)) (\lambda (t2: T).(eq T (THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)) t2)) (refl_equal T (THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3))) (lift h1 d1 (THead (Bind b) x2 x3)) (lift_bind b x2 x3 h1 d1)) (eq_ind_r T (THead (Bind b) (lift h2 d2 x2) (lift h2 (S d2) x3)) (\lambda (t2: T).(eq T (THead (Bind b) (lift h2 d2 x2) (lift h2 (S d2) x3)) t2)) (refl_equal T (THead (Bind b) (lift h2 d2 x2) (lift h2 (S d2) x3))) (lift h2 d2 (THead (Bind b) x2 x3)) (lift_bind b x2 x3 h2 d2))) t0 H13) x1 H12)))) (H0 x1 h1 h2 (S d1) (S d2) (le_S_n (S d1) (S d2) (lt_le_S (S d1) (S (S d2)) (lt_n_S d1 (S d2) (le_lt_n_Sm d1 d2 H1)))) H11)))) t H9) x0 H8)))) (H x0 h1 h2 d1 d2 H1 H6)) x H5)))))) (lift_gen_bind b (lift h1 d1 t) (lift h1 (S d1) t0) x h2 (plus d2 h1) H4))))) (\lambda (f: F).(\lambda (H3: (eq T (lift h1 d1 (THead (Flat f) t t0)) (lift h2 (plus d2 h1) x))).(let H4 \def (eq_ind T (lift h1 d1 (THead (Flat f) t t0)) (\lambda (t: T).(eq T t (lift h2 (plus d2 h1) x))) H3 (THead (Flat f) (lift h1 d1 t) (lift h1 d1 t0)) (lift_flat f t t0 h1 d1)) in (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h1 d1 t) (lift h2 (plus d2 h1) y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h1 d1 t0) (lift h2 (plus d2 h1) z)))) (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (THead (Flat f) t t0) (lift h2 d2 t2)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T x (THead (Flat f) x0 x1))).(\lambda (H6: (eq T (lift h1 d1 t) (lift h2 (plus d2 h1) x0))).(\lambda (H7: (eq T (lift h1 d1 t0) (lift h2 (plus d2 h1) x1))).(eq_ind_r T (THead (Flat f) x0 x1) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T t2 (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Flat f) t t0) (lift h2 d2 t3))))) (ex2_ind T (\lambda (t2: T).(eq T x0 (lift h1 d1 t2))) (\lambda (t2: T).(eq T t (lift h2 d2 t2))) (ex2 T (\lambda (t2: T).(eq T (THead (Flat f) x0 x1) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (THead (Flat f) t t0) (lift h2 d2 t2)))) (\lambda (x2: T).(\lambda (H8: (eq T x0 (lift h1 d1 x2))).(\lambda (H9: (eq T t (lift h2 d2 x2))).(eq_ind_r T (lift h1 d1 x2) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T (THead (Flat f) t2 x1) (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Flat f) t t0) (lift h2 d2 t3))))) (eq_ind_r T (lift h2 d2 x2) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T (THead (Flat f) (lift h1 d1 x2) x1) (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Flat f) t2 t0) (lift h2 d2 t3))))) (ex2_ind T (\lambda (t2: T).(eq T x1 (lift h1 d1 t2))) (\lambda (t2: T).(eq T t0 (lift h2 d2 t2))) (ex2 T (\lambda (t2: T).(eq T (THead (Flat f) (lift h1 d1 x2) x1) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (THead (Flat f) (lift h2 d2 x2) t0) (lift h2 d2 t2)))) (\lambda (x3: T).(\lambda (H10: (eq T x1 (lift h1 d1 x3))).(\lambda (H11: (eq T t0 (lift h2 d2 x3))).(eq_ind_r T (lift h1 d1 x3) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T (THead (Flat f) (lift h1 d1 x2) t2) (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Flat f) (lift h2 d2 x2) t0) (lift h2 d2 t3))))) (eq_ind_r T (lift h2 d2 x3) (\lambda (t2: T).(ex2 T (\lambda (t3: T).(eq T (THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)) (lift h1 d1 t3))) (\lambda (t3: T).(eq T (THead (Flat f) (lift h2 d2 x2) t2) (lift h2 d2 t3))))) (ex_intro2 T (\lambda (t2: T).(eq T (THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (THead (Flat f) (lift h2 d2 x2) (lift h2 d2 x3)) (lift h2 d2 t2))) (THead (Flat f) x2 x3) (eq_ind_r T (THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)) (\lambda (t2: T).(eq T (THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)) t2)) (refl_equal T (THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3))) (lift h1 d1 (THead (Flat f) x2 x3)) (lift_flat f x2 x3 h1 d1)) (eq_ind_r T (THead (Flat f) (lift h2 d2 x2) (lift h2 d2 x3)) (\lambda (t2: T).(eq T (THead (Flat f) (lift h2 d2 x2) (lift h2 d2 x3)) t2)) (refl_equal T (THead (Flat f) (lift h2 d2 x2) (lift h2 d2 x3))) (lift h2 d2 (THead (Flat f) x2 x3)) (lift_flat f x2 x3 h2 d2))) t0 H11) x1 H10)))) (H0 x1 h1 h2 d1 d2 H1 H7)) t H9) x0 H8)))) (H x0 h1 h2 d1 d2 H1 H6)) x H5)))))) (lift_gen_flat f (lift h1 d1 t) (lift h1 d1 t0) x h2 (plus d2 h1) H4))))) k H2))))))))))))) t1).

theorem lift_free:
 \forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d: nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k e (lift h d t)) (lift (plus k h) d t))))))))
\def
 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (k: nat).(\forall (d: nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k e (lift h d t0)) (lift (plus k h) d t0))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (_: (le e (plus d h))).(\lambda (_: (le d e)).(eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (lift k e t0) (lift (plus k h) d (TSort n)))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T t0 (lift (plus k h) d (TSort n)))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (TSort n) t0)) (refl_equal T (TSort n)) (lift (plus k h) d (TSort n)) (lift_sort n (plus k h) d)) (lift k e (TSort n)) (lift_sort n k e)) (lift h d (TSort n)) (lift_sort n h d))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (H: (le e (plus d h))).(\lambda (H0: (le d e)).(lt_le_e n d (eq T (lift k e (lift h d (TLRef n))) (lift (plus k h) d (TLRef n))) (\lambda (H1: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (lift k e t0) (lift (plus k h) d (TLRef n)))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 (lift (plus k h) d (TLRef n)))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (TLRef n) t0)) (refl_equal T (TLRef n)) (lift (plus k h) d (TLRef n)) (lift_lref_lt n (plus k h) d H1)) (lift k e (TLRef n)) (lift_lref_lt n k e (lt_le_trans n d e H1 H0))) (lift h d (TLRef n)) (lift_lref_lt n h d H1))) (\lambda (H1: (le d n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(eq T (lift k e t0) (lift (plus k h) d (TLRef n)))) (eq_ind_r T (TLRef (plus (plus n h) k)) (\lambda (t0: T).(eq T t0 (lift (plus k h) d (TLRef n)))) (eq_ind_r T (TLRef (plus n (plus k h))) (\lambda (t0: T).(eq T (TLRef (plus (plus n h) k)) t0)) (f_equal nat T TLRef (plus (plus n h) k) (plus n (plus k h)) (plus_permute_2_in_3_assoc n h k)) (lift (plus k h) d (TLRef n)) (lift_lref_ge n (plus k h) d H1)) (lift k e (TLRef (plus n h))) (lift_lref_ge (plus n h) k e (le_trans e (plus d h) (plus n h) H (plus_le_compat d n h h H1 (le_n h))))) (lift h d (TLRef n)) (lift_lref_ge n h d H1))))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (k: nat).(\forall (d: nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k e (lift h d t0)) (lift (plus k h) d t0)))))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (h: nat).(\forall (k: nat).(\forall (d: nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k e (lift h d t1)) (lift (plus k h) d t1)))))))))).(\lambda (h: nat).(\lambda (k0: nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (H1: (le e (plus d h))).(\lambda (H2: (le d e)).(eq_ind_r T (THead k (lift h d t0) (lift h (s k d) t1)) (\lambda (t2: T).(eq T (lift k0 e t2) (lift (plus k0 h) d (THead k t0 t1)))) (eq_ind_r T (THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))) (\lambda (t2: T).(eq T t2 (lift (plus k0 h) d (THead k t0 t1)))) (eq_ind_r T (THead k (lift (plus k0 h) d t0) (lift (plus k0 h) (s k d) t1)) (\lambda (t2: T).(eq T (THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))) t2)) (f_equal3 K T T T THead k k (lift k0 e (lift h d t0)) (lift (plus k0 h) d t0) (lift k0 (s k e) (lift h (s k d) t1)) (lift (plus k0 h) (s k d) t1) (refl_equal K k) (H h k0 d e H1 H2) (H0 h k0 (s k d) (s k e) (eq_ind nat (s k (plus d h)) (\lambda (n: nat).(le (s k e) n)) (s_le k e (plus d h) H1) (plus (s k d) h) (s_plus k d h)) (s_le k d e H2))) (lift (plus k0 h) d (THead k t0 t1)) (lift_head k t0 t1 (plus k0 h) d)) (lift k0 e (THead k (lift h d t0) (lift h (s k d) t1))) (lift_head k (lift h d t0) (lift h (s k d) t1) k0 e)) (lift h d (THead k t0 t1)) (lift_head k t0 t1 h d))))))))))))) t).

theorem lift_d:
 \forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (eq T (lift h (plus k d) (lift k e t)) (lift k e (lift h d t))))))))
\def
 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (k: nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (eq T (lift h (plus k d) (lift k e t0)) (lift k e (lift h d t0))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (_: (le e d)).(eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (lift h (plus k d) t0) (lift k e (lift h d (TSort n))))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T t0 (lift k e (lift h d (TSort n))))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (TSort n) (lift k e t0))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (TSort n) t0)) (refl_equal T (TSort n)) (lift k e (TSort n)) (lift_sort n k e)) (lift h d (TSort n)) (lift_sort n h d)) (lift h (plus k d) (TSort n)) (lift_sort n h (plus k d))) (lift k e (TSort n)) (lift_sort n k e)))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (H: (le e d)).(lt_le_e n e (eq T (lift h (plus k d) (lift k e (TLRef n))) (lift k e (lift h d (TLRef n)))) (\lambda (H0: (lt n e)).(let H1 \def (lt_le_trans n e d H0 H) in (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (lift h (plus k d) t0) (lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 (lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (TLRef n) (lift k e t0))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (TLRef n) t0)) (refl_equal T (TLRef n)) (lift k e (TLRef n)) (lift_lref_lt n k e H0)) (lift h d (TLRef n)) (lift_lref_lt n h d H1)) (lift h (plus k d) (TLRef n)) (lift_lref_lt n h (plus k d) (lt_le_trans n d (plus k d) H1 (le_plus_r k d)))) (lift k e (TLRef n)) (lift_lref_lt n k e H0)))) (\lambda (H0: (le e n)).(eq_ind_r T (TLRef (plus n k)) (\lambda (t0: T).(eq T (lift h (plus k d) t0) (lift k e (lift h d (TLRef n))))) (eq_ind_r nat (plus d k) (\lambda (n0: nat).(eq T (lift h n0 (TLRef (plus n k))) (lift k e (lift h d (TLRef n))))) (lt_le_e n d (eq T (lift h (plus d k) (TLRef (plus n k))) (lift k e (lift h d (TLRef n)))) (\lambda (H1: (lt n d)).(eq_ind_r T (TLRef (plus n k)) (\lambda (t0: T).(eq T t0 (lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (TLRef (plus n k)) (lift k e t0))) (eq_ind_r T (TLRef (plus n k)) (\lambda (t0: T).(eq T (TLRef (plus n k)) t0)) (refl_equal T (TLRef (plus n k))) (lift k e (TLRef n)) (lift_lref_ge n k e H0)) (lift h d (TLRef n)) (lift_lref_lt n h d H1)) (lift h (plus d k) (TLRef (plus n k))) (lift_lref_lt (plus n k) h (plus d k) (lt_le_S (plus n k) (plus d k) (plus_lt_compat_r n d k H1))))) (\lambda (H1: (le d n)).(eq_ind_r T (TLRef (plus (plus n k) h)) (\lambda (t0: T).(eq T t0 (lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(eq T (TLRef (plus (plus n k) h)) (lift k e t0))) (eq_ind_r T (TLRef (plus (plus n h) k)) (\lambda (t0: T).(eq T (TLRef (plus (plus n k) h)) t0)) (f_equal nat T TLRef (plus (plus n k) h) (plus (plus n h) k) (sym_eq nat (plus (plus n h) k) (plus (plus n k) h) (plus_permute_2_in_3 n h k))) (lift k e (TLRef (plus n h))) (lift_lref_ge (plus n h) k e (le_S_n e (plus n h) (lt_le_S e (S (plus n h)) (le_lt_n_Sm e (plus n h) (le_plus_trans e n h H0)))))) (lift h d (TLRef n)) (lift_lref_ge n h d H1)) (lift h (plus d k) (TLRef (plus n k))) (lift_lref_ge (plus n k) h (plus d k) (le_S_n (plus d k) (plus n k) (lt_le_S (plus d k) (S (plus n k)) (le_lt_n_Sm (plus d k) (plus n k) (plus_le_compat d n k k H1 (le_n k))))))))) (plus k d) (plus_comm k d)) (lift k e (TLRef n)) (lift_lref_ge n k e H0)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (k: nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (eq T (lift h (plus k d) (lift k e t0)) (lift k e (lift h d t0)))))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (h: nat).(\forall (k: nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (eq T (lift h (plus k d) (lift k e t1)) (lift k e (lift h d t1)))))))))).(\lambda (h: nat).(\lambda (k0: nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (H1: (le e d)).(eq_ind_r T (THead k (lift k0 e t0) (lift k0 (s k e) t1)) (\lambda (t2: T).(eq T (lift h (plus k0 d) t2) (lift k0 e (lift h d (THead k t0 t1))))) (eq_ind_r T (THead k (lift h (plus k0 d) (lift k0 e t0)) (lift h (s k (plus k0 d)) (lift k0 (s k e) t1))) (\lambda (t2: T).(eq T t2 (lift k0 e (lift h d (THead k t0 t1))))) (eq_ind_r T (THead k (lift h d t0) (lift h (s k d) t1)) (\lambda (t2: T).(eq T (THead k (lift h (plus k0 d) (lift k0 e t0)) (lift h (s k (plus k0 d)) (lift k0 (s k e) t1))) (lift k0 e t2))) (eq_ind_r T (THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))) (\lambda (t2: T).(eq T (THead k (lift h (plus k0 d) (lift k0 e t0)) (lift h (s k (plus k0 d)) (lift k0 (s k e) t1))) t2)) (eq_ind_r nat (plus k0 (s k d)) (\lambda (n: nat).(eq T (THead k (lift h (plus k0 d) (lift k0 e t0)) (lift h n (lift k0 (s k e) t1))) (THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))))) (f_equal3 K T T T THead k k (lift h (plus k0 d) (lift k0 e t0)) (lift k0 e (lift h d t0)) (lift h (plus k0 (s k d)) (lift k0 (s k e) t1)) (lift k0 (s k e) (lift h (s k d) t1)) (refl_equal K k) (H h k0 d e H1) (H0 h k0 (s k d) (s k e) (s_le k e d H1))) (s k (plus k0 d)) (s_plus_sym k k0 d)) (lift k0 e (THead k (lift h d t0) (lift h (s k d) t1))) (lift_head k (lift h d t0) (lift h (s k d) t1) k0 e)) (lift h d (THead k t0 t1)) (lift_head k t0 t1 h d)) (lift h (plus k0 d) (THead k (lift k0 e t0) (lift k0 (s k e) t1))) (lift_head k (lift k0 e t0) (lift k0 (s k e) t1) h (plus k0 d))) (lift k0 e (THead k t0 t1)) (lift_head k t0 t1 k0 e)))))))))))) t).

theorem lift_weight_map:
 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat (weight_map f (lift h d t)) (weight_map f t))))))
\def
 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat (weight_map f (lift h d t0)) (weight_map f t0))))))) (\lambda (n: nat).(\lambda (_: nat).(\lambda (d: nat).(\lambda (f: ((nat \to nat))).(\lambda (_: ((\forall (m: nat).((le d m) \to (eq nat (f m) O))))).(refl_equal nat (weight_map f (TSort n)))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to nat))).(\lambda (H: ((\forall (m: nat).((le d m) \to (eq nat (f m) O))))).(lt_le_e n d (eq nat (weight_map f (lift h d (TLRef n))) (weight_map f (TLRef n))) (\lambda (H0: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq nat (weight_map f t0) (weight_map f (TLRef n)))) (refl_equal nat (weight_map f (TLRef n))) (lift h d (TLRef n)) (lift_lref_lt n h d H0))) (\lambda (H0: (le d n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(eq nat (weight_map f t0) (weight_map f (TLRef n)))) (eq_ind_r nat O (\lambda (n0: nat).(eq nat (f (plus n h)) n0)) (H (plus n h) (le_S_n d (plus n h) (le_n_S d (plus n h) (le_plus_trans d n h H0)))) (f n) (H n H0)) (lift h d (TLRef n)) (lift_lref_ge n h d H0))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat (weight_map f (lift h d t0)) (weight_map f t0)))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat (weight_map f (lift h d t1)) (weight_map f t1)))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to nat))).(\lambda (H1: ((\forall (m: nat).((le d m) \to (eq nat (f m) O))))).(K_ind (\lambda (k0: K).(eq nat (weight_map f (lift h d (THead k0 t0 t1))) (weight_map f (THead k0 t0 t1)))) (\lambda (b: B).(eq_ind_r T (THead (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1)) (\lambda (t2: T).(eq nat (weight_map f t2) (weight_map f (THead (Bind b) t0 t1)))) (B_ind (\lambda (b0: B).(eq nat (match b0 with [Abbr \Rightarrow (S (plus (weight_map f (lift h d t0)) (weight_map (wadd f (S (weight_map f (lift h d t0)))) (lift h (S d) t1)))) | Abst \Rightarrow (S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1)))) | Void \Rightarrow (S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1))))]) (match b0 with [Abbr \Rightarrow (S (plus (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1))) | Abst \Rightarrow (S (plus (weight_map f t0) (weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus (weight_map f t0) (weight_map (wadd f O) t1)))]))) (eq_ind_r nat (weight_map f t0) (\lambda (n: nat).(eq nat (S (plus n (weight_map (wadd f (S n)) (lift h (S d) t1)))) (S (plus (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1))))) (eq_ind_r nat (weight_map (wadd f (S (weight_map f t0))) t1) (\lambda (n: nat).(eq nat (S (plus (weight_map f t0) n)) (S (plus (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1))))) (refl_equal nat (S (plus (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)))) (weight_map (wadd f (S (weight_map f t0))) (lift h (S d) t1)) (H0 h (S d) (wadd f (S (weight_map f t0))) (\lambda (m: nat).(\lambda (H2: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d n)) (eq nat (wadd f (S (weight_map f t0)) m) O) (\lambda (x: nat).(\lambda (H3: (eq nat m (S x))).(\lambda (H4: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd f (S (weight_map f t0)) n) O)) (H1 x H4) m H3)))) (le_gen_S d m H2)))))) (weight_map f (lift h d t0)) (H h d f H1)) (eq_ind_r nat (weight_map (wadd f O) t1) (\lambda (n: nat).(eq nat (S (plus (weight_map f (lift h d t0)) n)) (S (plus (weight_map f t0) (weight_map (wadd f O) t1))))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) t1)) (plus (weight_map f t0) (weight_map (wadd f O) t1)) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map f t0) (weight_map (wadd f O) t1) (weight_map (wadd f O) t1) (H h d f H1) (refl_equal nat (weight_map (wadd f O) t1)))) (weight_map (wadd f O) (lift h (S d) t1)) (H0 h (S d) (wadd f O) (\lambda (m: nat).(\lambda (H2: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d n)) (eq nat (wadd f O m) O) (\lambda (x: nat).(\lambda (H3: (eq nat m (S x))).(\lambda (H4: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd f O n) O)) (H1 x H4) m H3)))) (le_gen_S d m H2)))))) (eq_ind_r nat (weight_map (wadd f O) t1) (\lambda (n: nat).(eq nat (S (plus (weight_map f (lift h d t0)) n)) (S (plus (weight_map f t0) (weight_map (wadd f O) t1))))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) t1)) (plus (weight_map f t0) (weight_map (wadd f O) t1)) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map f t0) (weight_map (wadd f O) t1) (weight_map (wadd f O) t1) (H h d f H1) (refl_equal nat (weight_map (wadd f O) t1)))) (weight_map (wadd f O) (lift h (S d) t1)) (H0 h (S d) (wadd f O) (\lambda (m: nat).(\lambda (H2: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d n)) (eq nat (wadd f O m) O) (\lambda (x: nat).(\lambda (H3: (eq nat m (S x))).(\lambda (H4: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd f O n) O)) (H1 x H4) m H3)))) (le_gen_S d m H2)))))) b) (lift h d (THead (Bind b) t0 t1)) (lift_head (Bind b) t0 t1 h d))) (\lambda (f0: F).(eq_ind_r T (THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) d) t1)) (\lambda (t2: T).(eq nat (weight_map f t2) (weight_map f (THead (Flat f0) t0 t1)))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map f (lift h d t1))) (plus (weight_map f t0) (weight_map f t1)) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map f t0) (weight_map f (lift h d t1)) (weight_map f t1) (H h d f H1) (H0 h d f H1))) (lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d))) k)))))))))) t).

theorem lift_weight:
 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq nat (weight (lift h d t)) (weight t))))
\def
 \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(lift_weight_map t h d (\lambda (_: nat).O) (\lambda (m: nat).(\lambda (_: (le d m)).(refl_equal nat O)))))).

theorem lift_weight_add:
 \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m))))) \to (eq nat (weight_map f (lift h d t)) (weight_map g (lift (S h) d t)))))))))))
\def
 \lambda (w: nat).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m))))) \to (eq nat (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0))))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m)))))).(\lambda (_: (eq nat (g d) w)).(\lambda (_: ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m)))))).(refl_equal nat (weight_map g (lift (S h) d (TSort n)))))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: ((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m)))))).(\lambda (_: (eq nat (g d) w)).(\lambda (H1: ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m)))))).(lt_le_e n d (eq nat (weight_map f (lift h d (TLRef n))) (weight_map g (lift (S h) d (TLRef n)))) (\lambda (H2: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq nat (weight_map f t0) (weight_map g (lift (S h) d (TLRef n))))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq nat (weight_map f (TLRef n)) (weight_map g t0))) (sym_equal nat (g n) (f n) (H n H2)) (lift (S h) d (TLRef n)) (lift_lref_lt n (S h) d H2)) (lift h d (TLRef n)) (lift_lref_lt n h d H2))) (\lambda (H2: (le d n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(eq nat (weight_map f t0) (weight_map g (lift (S h) d (TLRef n))))) (eq_ind_r T (TLRef (plus n (S h))) (\lambda (t0: T).(eq nat (weight_map f (TLRef (plus n h))) (weight_map g t0))) (eq_ind nat (S (plus n h)) (\lambda (n0: nat).(eq nat (f (plus n h)) (g n0))) (sym_equal nat (g (S (plus n h))) (f (plus n h)) (H1 (plus n h) (le_plus_trans d n h H2))) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) d (TLRef n)) (lift_lref_ge n (S h) d H2)) (lift h d (TLRef n)) (lift_lref_ge n h d H2)))))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m))))) \to (eq nat (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)))))))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m))))) \to (eq nat (weight_map f (lift h d t1)) (weight_map g (lift (S h) d t1)))))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m)))))).(\lambda (H2: (eq nat (g d) w)).(\lambda (H3: ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m)))))).(K_ind (\lambda (k0: K).(eq nat (weight_map f (lift h d (THead k0 t0 t1))) (weight_map g (lift (S h) d (THead k0 t0 t1))))) (\lambda (b: B).(eq_ind_r T (THead (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1)) (\lambda (t2: T).(eq nat (weight_map f t2) (weight_map g (lift (S h) d (THead (Bind b) t0 t1))))) (eq_ind_r T (THead (Bind b) (lift (S h) d t0) (lift (S h) (s (Bind b) d) t1)) (\lambda (t2: T).(eq nat (weight_map f (THead (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1))) (weight_map g t2))) (B_ind (\lambda (b0: B).(eq nat (match b0 with [Abbr \Rightarrow (S (plus (weight_map f (lift h d t0)) (weight_map (wadd f (S (weight_map f (lift h d t0)))) (lift h (S d) t1)))) | Abst \Rightarrow (S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1)))) | Void \Rightarrow (S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1))))]) (match b0 with [Abbr \Rightarrow (S (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd g (S (weight_map g (lift (S h) d t0)))) (lift (S h) (S d) t1)))) | Abst \Rightarrow (S (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S h) (S d) t1)))) | Void \Rightarrow (S (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S h) (S d) t1))))]))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map (wadd f (S (weight_map f (lift h d t0)))) (lift h (S d) t1))) (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd g (S (weight_map g (lift (S h) d t0)))) (lift (S h) (S d) t1))) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)) (weight_map (wadd f (S (weight_map f (lift h d t0)))) (lift h (S d) t1)) (weight_map (wadd g (S (weight_map g (lift (S h) d t0)))) (lift (S h) (S d) t1)) (H h d f g H1 H2 H3) (H0 h (S d) (wadd f (S (weight_map f (lift h d t0)))) (wadd g (S (weight_map g (lift (S h) d t0)))) (\lambda (m: nat).(\lambda (H4: (lt m (S d))).(or_ind (eq nat m O) (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g (S (weight_map g (lift (S h) d t0))) m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda (H5: (eq nat m O)).(eq_ind_r nat O (\lambda (n: nat).(eq nat (wadd g (S (weight_map g (lift (S h) d t0))) n) (wadd f (S (weight_map f (lift h d t0))) n))) (f_equal nat nat S (weight_map g (lift (S h) d t0)) (weight_map f (lift h d t0)) (sym_equal nat (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)) (H h d f g H1 H2 H3))) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m: nat).(lt m d)))).(ex2_ind nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g (S (weight_map g (lift (S h) d t0))) m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7: (lt x d)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd g (S (weight_map g (lift (S h) d t0))) n) (wadd f (S (weight_map f (lift h d t0))) n))) (H1 x H7) m H6)))) H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d n)) (eq nat (g m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda (x: nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (g n) (wadd f (S (weight_map f (lift h d t0))) n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1))) (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S h) (S d) t1))) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)) (weight_map (wadd f O) (lift h (S d) t1)) (weight_map (wadd g O) (lift (S h) (S d) t1)) (H h d f g H1 H2 H3) (H0 h (S d) (wadd f O) (wadd g O) (\lambda (m: nat).(\lambda (H4: (lt m (S d))).(or_ind (eq nat m O) (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g O m) (wadd f O m)) (\lambda (H5: (eq nat m O)).(eq_ind_r nat O (\lambda (n: nat).(eq nat (wadd g O n) (wadd f O n))) (refl_equal nat O) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m: nat).(lt m d)))).(ex2_ind nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g O m) (wadd f O m)) (\lambda (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7: (lt x d)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd g O n) (wadd f O n))) (H1 x H7) m H6)))) H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d n)) (eq nat (g m) (wadd f O m)) (\lambda (x: nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (g n) (wadd f O n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1))) (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S h) (S d) t1))) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)) (weight_map (wadd f O) (lift h (S d) t1)) (weight_map (wadd g O) (lift (S h) (S d) t1)) (H h d f g H1 H2 H3) (H0 h (S d) (wadd f O) (wadd g O) (\lambda (m: nat).(\lambda (H4: (lt m (S d))).(or_ind (eq nat m O) (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g O m) (wadd f O m)) (\lambda (H5: (eq nat m O)).(eq_ind_r nat O (\lambda (n: nat).(eq nat (wadd g O n) (wadd f O n))) (refl_equal nat O) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m: nat).(lt m d)))).(ex2_ind nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g O m) (wadd f O m)) (\lambda (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7: (lt x d)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd g O n) (wadd f O n))) (H1 x H7) m H6)))) H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d n)) (eq nat (g m) (wadd f O m)) (\lambda (x: nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (g n) (wadd f O n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) b) (lift (S h) d (THead (Bind b) t0 t1)) (lift_head (Bind b) t0 t1 (S h) d)) (lift h d (THead (Bind b) t0 t1)) (lift_head (Bind b) t0 t1 h d))) (\lambda (f0: F).(eq_ind_r T (THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) d) t1)) (\lambda (t2: T).(eq nat (weight_map f t2) (weight_map g (lift (S h) d (THead (Flat f0) t0 t1))))) (eq_ind_r T (THead (Flat f0) (lift (S h) d t0) (lift (S h) (s (Flat f0) d) t1)) (\lambda (t2: T).(eq nat (weight_map f (THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) d) t1))) (weight_map g t2))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map f (lift h d t1))) (plus (weight_map g (lift (S h) d t0)) (weight_map g (lift (S h) d t1))) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)) (weight_map f (lift h d t1)) (weight_map g (lift (S h) d t1)) (H h d f g H1 H2 H3) (H0 h d f g H1 H2 H3))) (lift (S h) d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 (S h) d)) (lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d))) k))))))))))))) t)).

theorem lift_weight_add_O:
 \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (f: ((nat \to nat))).(eq nat (weight_map f (lift h O t)) (weight_map (wadd f w) (lift (S h) O t))))))
\def
 \lambda (w: nat).(\lambda (t: T).(\lambda (h: nat).(\lambda (f: ((nat \to nat))).(lift_weight_add (plus (wadd f w O) O) t h O f (wadd f w) (\lambda (m: nat).(\lambda (H: (lt m O)).(let H0 \def (match H return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to (eq nat (wadd f w m) (f m))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) O)).(let H1 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat (wadd f w m) (f m)) H1))) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) O)).((let H2 \def (eq_ind nat (S m0) (\lambda (e: nat).(match e return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S m) m0) \to (eq nat (wadd f w m) (f m))) H2)) H0))]) in (H0 (refl_equal nat O))))) (plus_n_O (wadd f w O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal nat (f m)))))))).

theorem lift_tlt_dx:
 \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).(tlt t (THead k u (lift h d t)))))))
\def
 \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(eq_ind nat (weight (lift h d t)) (\lambda (n: nat).(lt n (weight (THead k u (lift h d t))))) (tlt_head_dx k u (lift h d t)) (weight t) (lift_weight t h d)))))).

inductive PList: Set \def
| PNil: PList
| PCons: nat \to (nat \to (PList \to PList)).

definition PConsTail:
 PList \to (nat \to (nat \to PList))
\def
 let rec PConsTail (hds: PList) on hds: (nat \to (nat \to PList)) \def (\lambda (h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow (PCons h0 d0 PNil) | (PCons h d hds0) \Rightarrow (PCons h d (PConsTail hds0 h0 d0))]))) in PConsTail.

definition trans:
 PList \to (nat \to nat)
\def
 let rec trans (hds: PList) on hds: (nat \to nat) \def (\lambda (i: nat).(match hds with [PNil \Rightarrow i | (PCons h d hds0) \Rightarrow (let j \def (trans hds0 i) in (match (blt j d) with [true \Rightarrow j | false \Rightarrow (plus j h)]))])) in trans.

definition Ss:
 PList \to PList
\def
 let rec Ss (hds: PList) on hds: PList \def (match hds with [PNil \Rightarrow PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))]) in Ss.

definition lift1:
 PList \to (T \to T)
\def
 let rec lift1 (hds: PList) on hds: (T \to T) \def (\lambda (t: T).(match hds with [PNil \Rightarrow t | (PCons h d hds0) \Rightarrow (lift h d (lift1 hds0 t))])) in lift1.

definition lifts1:
 PList \to (TList \to TList)
\def
 let rec lifts1 (hds: PList) (ts: TList) on ts: TList \def (match ts with [TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift1 hds t) (lifts1 hds ts0))]) in lifts1.

theorem lift1_lref:
 \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef (trans hds i))))
\def
 \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: nat).(eq T (lift1 p (TLRef i)) (TLRef (trans p i))))) (\lambda (i: nat).(refl_equal T (TLRef (trans PNil i)))) (\lambda (h: nat).(\lambda (d: nat).(\lambda (p: PList).(\lambda (H: ((\forall (i: nat).(eq T (lift1 p (TLRef i)) (TLRef (trans p i)))))).(\lambda (i: nat).(eq_ind_r T (TLRef (trans p i)) (\lambda (t: T).(eq T (lift h d t) (TLRef (match (blt (trans p i) d) with [true \Rightarrow (trans p i) | false \Rightarrow (plus (trans p i) h)])))) (refl_equal T (TLRef (match (blt (trans p i) d) with [true \Rightarrow (trans p i) | false \Rightarrow (plus (trans p i) h)]))) (lift1 p (TLRef i)) (H i))))))) hds).

theorem lift1_bind:
 \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T (lift1 hds (THead (Bind b) u t)) (THead (Bind b) (lift1 hds u) (lift1 (Ss hds) t))))))
\def
 \lambda (b: B).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b) (lift1 p u) (lift1 (Ss p) t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal T (THead (Bind b) (lift1 PNil u) (lift1 (Ss PNil) t))))) (\lambda (h: nat).(\lambda (d: nat).(\lambda (p: PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))))))).(\lambda (u: T).(\lambda (t: T).(eq_ind_r T (THead (Bind b) (lift1 p u) (lift1 (Ss p) t)) (\lambda (t0: T).(eq T (lift h d t0) (THead (Bind b) (lift h d (lift1 p u)) (lift h (S d) (lift1 (Ss p) t))))) (eq_ind_r T (THead (Bind b) (lift h d (lift1 p u)) (lift h (S d) (lift1 (Ss p) t))) (\lambda (t0: T).(eq T t0 (THead (Bind b) (lift h d (lift1 p u)) (lift h (S d) (lift1 (Ss p) t))))) (refl_equal T (THead (Bind b) (lift h d (lift1 p u)) (lift h (S d) (lift1 (Ss p) t)))) (lift h d (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))) (lift_bind b (lift1 p u) (lift1 (Ss p) t) h d)) (lift1 p (THead (Bind b) u t)) (H u t)))))))) hds)).

theorem lift1_flat:
 \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T (lift1 hds (THead (Flat f) u t)) (THead (Flat f) (lift1 hds u) (lift1 hds t))))))
\def
 \lambda (f: F).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal T (THead (Flat f) (lift1 PNil u) (lift1 PNil t))))) (\lambda (h: nat).(\lambda (d: nat).(\lambda (p: PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p t))))))).(\lambda (u: T).(\lambda (t: T).(eq_ind_r T (THead (Flat f) (lift1 p u) (lift1 p t)) (\lambda (t0: T).(eq T (lift h d t0) (THead (Flat f) (lift h d (lift1 p u)) (lift h d (lift1 p t))))) (eq_ind_r T (THead (Flat f) (lift h d (lift1 p u)) (lift h d (lift1 p t))) (\lambda (t0: T).(eq T t0 (THead (Flat f) (lift h d (lift1 p u)) (lift h d (lift1 p t))))) (refl_equal T (THead (Flat f) (lift h d (lift1 p u)) (lift h d (lift1 p t)))) (lift h d (THead (Flat f) (lift1 p u) (lift1 p t))) (lift_flat f (lift1 p u) (lift1 p t) h d)) (lift1 p (THead (Flat f) u t)) (H u t)))))))) hds)).

theorem lift1_cons_tail:
 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))))))
\def
 \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(eq T (lift1 (PConsTail p h d) t) (lift1 p (lift h d t)))) (refl_equal T (lift h d t)) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1 (PConsTail p h d) t) (lift1 p (lift h d t)))).(eq_ind_r T (lift1 p (lift h d t)) (\lambda (t0: T).(eq T (lift n n0 t0) (lift n n0 (lift1 p (lift h d t))))) (refl_equal T (lift n n0 (lift1 p (lift h d t)))) (lift1 (PConsTail p h d) t) H))))) hds)))).

theorem lifts1_flat:
 \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts: TList).(eq T (lift1 hds (THeads (Flat f) ts t)) (THeads (Flat f) (lifts1 hds ts) (lift1 hds t))))))
\def
 \lambda (f: F).(\lambda (hds: PList).(\lambda (t: T).(\lambda (ts: TList).(TList_ind (\lambda (t0: TList).(eq T (lift1 hds (THeads (Flat f) t0 t)) (THeads (Flat f) (lifts1 hds t0) (lift1 hds t)))) (refl_equal T (lift1 hds t)) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (eq T (lift1 hds (THeads (Flat f) t1 t)) (THeads (Flat f) (lifts1 hds t1) (lift1 hds t)))).(eq_ind_r T (THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f) t1 t))) (\lambda (t2: T).(eq T t2 (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1) (lift1 hds t))))) (eq_ind_r T (THeads (Flat f) (lifts1 hds t1) (lift1 hds t)) (\lambda (t2: T).(eq T (THead (Flat f) (lift1 hds t0) t2) (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1) (lift1 hds t))))) (refl_equal T (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1) (lift1 hds t)))) (lift1 hds (THeads (Flat f) t1 t)) H) (lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))) (lift1_flat f hds t0 (THeads (Flat f) t1 t)))))) ts)))).

theorem lifts1_nil:
 \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
\def
 \lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 PNil t) t)) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: (eq TList (lifts1 PNil t0) t0)).(eq_ind_r TList t0 (\lambda (t1: TList).(eq TList (TCons t t1) (TCons t t0))) (refl_equal TList (TCons t t0)) (lifts1 PNil t0) H)))) ts).

theorem lifts1_cons:
 \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts: TList).(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))))))
\def
 \lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(\lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 (PCons h d hds) t) (lifts h d (lifts1 hds t)))) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: (eq TList (lifts1 (PCons h d hds) t0) (lifts h d (lifts1 hds t0)))).(eq_ind_r TList (lifts h d (lifts1 hds t0)) (\lambda (t1: TList).(eq TList (TCons (lift h d (lift1 hds t)) t1) (TCons (lift h d (lift1 hds t)) (lifts h d (lifts1 hds t0))))) (refl_equal TList (TCons (lift h d (lift1 hds t)) (lifts h d (lifts1 hds t0)))) (lifts1 (PCons h d hds) t0) H)))) ts)))).

theorem lift1_xhg:
 \forall (hds: PList).(\forall (t: T).(eq T (lift1 (Ss hds) (lift (S O) O t)) (lift (S O) O (lift1 hds t))))
\def
 \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (t: T).(eq T (lift1 (Ss p) (lift (S O) O t)) (lift (S O) O (lift1 p t))))) (\lambda (t: T).(refl_equal T (lift (S O) O t))) (\lambda (h: nat).(\lambda (d: nat).(\lambda (p: PList).(\lambda (H: ((\forall (t: T).(eq T (lift1 (Ss p) (lift (S O) O t)) (lift (S O) O (lift1 p t)))))).(\lambda (t: T).(eq_ind_r T (lift (S O) O (lift1 p t)) (\lambda (t0: T).(eq T (lift h (S d) t0) (lift (S O) O (lift h d (lift1 p t))))) (eq_ind nat (plus (S O) d) (\lambda (n: nat).(eq T (lift h n (lift (S O) O (lift1 p t))) (lift (S O) O (lift h d (lift1 p t))))) (eq_ind_r T (lift (S O) O (lift h d (lift1 p t))) (\lambda (t0: T).(eq T t0 (lift (S O) O (lift h d (lift1 p t))))) (refl_equal T (lift (S O) O (lift h d (lift1 p t)))) (lift h (plus (S O) d) (lift (S O) O (lift1 p t))) (lift_d (lift1 p t) h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S d))) (lift1 (Ss p) (lift (S O) O t)) (H t))))))) hds).

theorem lifts1_xhg:
 \forall (hds: PList).(\forall (ts: TList).(eq TList (lifts1 (Ss hds) (lifts (S O) O ts)) (lifts (S O) O (lifts1 hds ts))))
\def
 \lambda (hds: PList).(\lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 (Ss hds) (lifts (S O) O t)) (lifts (S O) O (lifts1 hds t)))) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: (eq TList (lifts1 (Ss hds) (lifts (S O) O t0)) (lifts (S O) O (lifts1 hds t0)))).(eq_ind_r T (lift (S O) O (lift1 hds t)) (\lambda (t1: T).(eq TList (TCons t1 (lifts1 (Ss hds) (lifts (S O) O t0))) (TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))))) (eq_ind_r TList (lifts (S O) O (lifts1 hds t0)) (\lambda (t1: TList).(eq TList (TCons (lift (S O) O (lift1 hds t)) t1) (TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))))) (refl_equal TList (TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0)))) (lifts1 (Ss hds) (lifts (S O) O t0)) H) (lift1 (Ss hds) (lift (S O) O t)) (lift1_xhg hds t))))) ts)).

inductive cnt: T \to Prop \def
| cnt_sort: \forall (n: nat).(cnt (TSort n))
| cnt_head: \forall (t: T).((cnt t) \to (\forall (k: K).(\forall (v: T).(cnt (THead k v t))))).

theorem cnt_lift:
 \forall (t: T).((cnt t) \to (\forall (i: nat).(\forall (d: nat).(cnt (lift i d t)))))
\def
 \lambda (t: T).(\lambda (H: (cnt t)).(cnt_ind (\lambda (t0: T).(\forall (i: nat).(\forall (d: nat).(cnt (lift i d t0))))) (\lambda (n: nat).(\lambda (i: nat).(\lambda (d: nat).(eq_ind_r T (TSort n) (\lambda (t0: T).(cnt t0)) (cnt_sort n) (lift i d (TSort n)) (lift_sort n i d))))) (\lambda (t0: T).(\lambda (_: (cnt t0)).(\lambda (H1: ((\forall (i: nat).(\forall (d: nat).(cnt (lift i d t0)))))).(\lambda (k: K).(\lambda (v: T).(\lambda (i: nat).(\lambda (d: nat).(eq_ind_r T (THead k (lift i d v) (lift i (s k d) t0)) (\lambda (t1: T).(cnt t1)) (cnt_head (lift i (s k d) t0) (H1 i (s k d)) k (lift i d v)) (lift i d (THead k v t0)) (lift_head k v t0 i d))))))))) t H)).