-definition r: K \to (nat \to nat) \def \lambda (k: K).(\lambda (i: nat).(match k with [(Bind _) \Rightarrow i | (Flat _) \Rightarrow (S i)])).
-
-definition clen: C \to nat \def let rec clen (c: C): nat \def (match c with [(CSort _) \Rightarrow O | (CHead c0 k _) \Rightarrow (s k (clen c0))]) in clen.
-
-axiom r_S: \forall (k: K).(\forall (i: nat).(eq nat (r k (S i)) (S (r k i)))) .
-
-axiom r_plus: \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k (plus i j)) (plus (r k i) j)))) .
-
-axiom r_plus_sym: \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k (plus i j)) (plus i (r k j))))) .
-
-axiom r_minus: \forall (i: nat).(\forall (n: nat).((lt n i) \to (\forall (k: K).(eq nat (minus (r k i) (S n)) (r k (minus i (S n))))))) .
-
-axiom r_dis: \forall (k: K).(\forall (P: Prop).(((((\forall (i: nat).(eq nat (r k i) i))) \to P)) \to (((((\forall (i: nat).(eq nat (r k i) (S i)))) \to P)) \to P))) .
-
-axiom s_r: \forall (k: K).(\forall (i: nat).(eq nat (s k (r k i)) (S i))) .
-
-axiom r_arith0: \forall (k: K).(\forall (i: nat).(eq nat (minus (r k (S i)) (S O)) (r k i))) .
-
-axiom r_arith1: \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (minus (r k (S i)) (S j)) (minus (r k i) j)))) .
-
-definition tweight: T \to nat \def let rec tweight (t: T): nat \def (match t with [(TSort _) \Rightarrow (S O) | (TLRef _) \Rightarrow (S O) | (THead _ u t0) \Rightarrow (S (plus (tweight u) (tweight t0)))]) in tweight.
-
-definition cweight: C \to nat \def let rec cweight (c: C): nat \def (match c with [(CSort _) \Rightarrow O | (CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))]) in cweight.
-
-definition clt: C \to (C \to Prop) \def \lambda (c1: C).(\lambda (c2: C).(lt (cweight c1) (cweight c2))).
-
-definition cle: C \to (C \to Prop) \def \lambda (c1: C).(\lambda (c2: C).(le (cweight c1) (cweight c2))).
-
-axiom tweight_lt: \forall (t: T).(lt O (tweight t)) .
-
-axiom clt_cong: \forall (c: C).(\forall (d: C).((clt c d) \to (\forall (k: K).(\forall (t: T).(clt (CHead c k t) (CHead d k t)))))) .
-
-axiom clt_head: \forall (k: K).(\forall (c: C).(\forall (u: T).(clt c (CHead c k u)))) .
-
-axiom clt_wf__q_ind: \forall (P: ((C \to Prop))).(((\forall (n: nat).((\lambda (P: ((C \to Prop))).(\lambda (n0: nat).(\forall (c: C).((eq nat (cweight c) n0) \to (P c))))) P n))) \to (\forall (c: C).(P c))) .
-
-axiom clt_wf_ind: \forall (P: ((C \to Prop))).(((\forall (c: C).(((\forall (d: C).((clt d c) \to (P d)))) \to (P c)))) \to (\forall (c: C).(P c))) .
-
-definition CTail: K \to (T \to (C \to C)) \def let rec CTail (k: K) (t: T) (c: C): C \def (match c with [(CSort n) \Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead (CTail k t d) h u)]) in CTail.
-
-axiom chead_ctail: \forall (c: C).(\forall (t: T).(\forall (k: K).(ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c k t) (CTail h u d)))))))) .
-
-axiom clt_thead: \forall (k: K).(\forall (u: T).(\forall (c: C).(clt c (CTail k u c)))) .
-
-axiom c_tail_ind: \forall (P: ((C \to Prop))).(((\forall (n: nat).(P (CSort n)))) \to (((\forall (c: C).((P c) \to (\forall (k: K).(\forall (t: T).(P (CTail k t c))))))) \to (\forall (c: C).(P c)))) .
-
-definition fweight: C \to (T \to nat) \def \lambda (c: C).(\lambda (t: T).(plus (cweight c) (tweight t))).
-
-definition flt: C \to (T \to (C \to (T \to Prop))) \def \lambda (c1: C).(\lambda (t1: T).(\lambda (c2: C).(\lambda (t2: T).(lt (fweight c1 t1) (fweight c2 t2))))).
-
-axiom flt_thead_sx: \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c u c (THead k u t))))) .
-
-axiom flt_thead_dx: \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c t c (THead k u t))))) .
-
-axiom flt_shift: \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt (CHead c k u) t c (THead k u t))))) .
-
-axiom flt_arith0: \forall (k: K).(\forall (c: C).(\forall (t: T).(\forall (i: nat).(flt c t (CHead c k t) (TLRef i))))) .
-
-axiom flt_arith1: \forall (k1: K).(\forall (c1: C).(\forall (c2: C).(\forall (t1: T).((cle (CHead c1 k1 t1) c2) \to (\forall (k2: K).(\forall (t2: T).(\forall (i: nat).(flt c1 t1 (CHead c2 k2 t2) (TLRef i))))))))) .
-
-axiom flt_arith2: \forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (i: nat).((flt c1 t1 c2 (TLRef i)) \to (\forall (k2: K).(\forall (t2: T).(\forall (j: nat).(flt c1 t1 (CHead c2 k2 t2) (TLRef j))))))))) .
-
-axiom flt_wf__q_ind: \forall (P: ((C \to (T \to Prop)))).(((\forall (n: nat).((\lambda (P: ((C \to (T \to Prop)))).(\lambda (n0: nat).(\forall (c: C).(\forall (t: T).((eq nat (fweight c t) n0) \to (P c t)))))) P n))) \to (\forall (c: C).(\forall (t: T).(P c t)))) .
-
-axiom flt_wf_ind: \forall (P: ((C \to (T \to Prop)))).(((\forall (c2: C).(\forall (t2: T).(((\forall (c1: C).(\forall (t1: T).((flt c1 t1 c2 t2) \to (P c1 t1))))) \to (P c2 t2))))) \to (\forall (c: C).(\forall (t: T).(P c t)))) .
-
-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): 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): TList \def (match ts with [TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift h d t) (lifts h d ts0))]) in lifts.
-
-axiom lift_sort: \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (TSort n)) (TSort n)))) .
-
-axiom 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))))) .
-
-axiom 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)))))) .
-
-axiom 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))))))) .
-
-axiom 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))))))) .
-
-axiom 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))))))) .
-
-axiom 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)))))) .
-
-axiom 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))))))))) .
-
-axiom 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))))))) .
-
-axiom 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))))))) .
-
-axiom 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))))))) .
-
-axiom 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))))))))))) .
-
-axiom 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))))))))))) .
-
-axiom 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))))))))))) .
-
-axiom 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)))))) .
-
-axiom lift_r: \forall (t: T).(\forall (d: nat).(eq T (lift O d t) t)) .
-
-axiom lift_lref_gt: \forall (d: nat).(\forall (n: nat).((lt d n) \to (eq T (lift (S O) d (TLRef (pred n))) (TLRef n)))) .
-
-axiom 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))))) .
-
-axiom 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))))))))))) .
-
-axiom 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)))))))) .
-
-axiom 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)))))))) .
-
-axiom 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)))))) .
-
-axiom lift_weight: \forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq nat (weight (lift h d t)) (weight t)))) .
-
-axiom 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))))))))))) .
-
-axiom 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)))))) .
-
-axiom 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))))))) .
+definition r:
+ K \to (nat \to nat)
+\def
+ \lambda (k: K).(\lambda (i: nat).(match k with [(Bind _) \Rightarrow i | (Flat _) \Rightarrow (S i)])).
+
+definition clen:
+ C \to nat
+\def
+ let rec clen (c: C) on c: nat \def (match c with [(CSort _) \Rightarrow O | (CHead c0 k _) \Rightarrow (s k (clen c0))]) in clen.
+
+theorem r_S:
+ \forall (k: K).(\forall (i: nat).(eq nat (r k (S i)) (S (r k i))))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(eq nat (r k0 (S i)) (S (r k0 i))))) (\lambda (b: B).(\lambda (i: nat).(refl_equal nat (S (r (Bind b) i))))) (\lambda (f: F).(\lambda (i: nat).(refl_equal nat (S (r (Flat f) i))))) k).
+
+theorem r_plus:
+ \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k (plus i j)) (plus (r k i) j))))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k0 (plus i j)) (plus (r k0 i) j))))) (\lambda (b: B).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (plus (r (Bind b) i) j))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (plus (r (Flat f) i) j))))) k).
+
+theorem r_plus_sym:
+ \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k (plus i j)) (plus i (r k j)))))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k0 (plus i j)) (plus i (r k0 j)))))) (\lambda (_: B).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (plus i j))))) (\lambda (_: F).(\lambda (i: nat).(\lambda (j: nat).(plus_n_Sm i j)))) k).
+
+theorem r_minus:
+ \forall (i: nat).(\forall (n: nat).((lt n i) \to (\forall (k: K).(eq nat (minus (r k i) (S n)) (r k (minus i (S n)))))))
+\def
+ \lambda (i: nat).(\lambda (n: nat).(\lambda (H: (lt n i)).(\lambda (k: K).(K_ind (\lambda (k0: K).(eq nat (minus (r k0 i) (S n)) (r k0 (minus i (S n))))) (\lambda (_: B).(refl_equal nat (minus i (S n)))) (\lambda (_: F).(minus_x_Sy i n H)) k)))).
+
+theorem r_dis:
+ \forall (k: K).(\forall (P: Prop).(((((\forall (i: nat).(eq nat (r k i) i))) \to P)) \to (((((\forall (i: nat).(eq nat (r k i) (S i)))) \to P)) \to P)))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (P: Prop).(((((\forall (i: nat).(eq nat (r k0 i) i))) \to P)) \to (((((\forall (i: nat).(eq nat (r k0 i) (S i)))) \to P)) \to P)))) (\lambda (b: B).(\lambda (P: Prop).(\lambda (H: ((((\forall (i: nat).(eq nat (r (Bind b) i) i))) \to P))).(\lambda (_: ((((\forall (i: nat).(eq nat (r (Bind b) i) (S i)))) \to P))).(H (\lambda (i: nat).(refl_equal nat i))))))) (\lambda (f: F).(\lambda (P: Prop).(\lambda (_: ((((\forall (i: nat).(eq nat (r (Flat f) i) i))) \to P))).(\lambda (H0: ((((\forall (i: nat).(eq nat (r (Flat f) i) (S i)))) \to P))).(H0 (\lambda (i: nat).(refl_equal nat (S i)))))))) k).
+
+theorem s_r:
+ \forall (k: K).(\forall (i: nat).(eq nat (s k (r k i)) (S i)))
+\def
+ \lambda (k: K).(match k return (\lambda (k0: K).(\forall (i: nat).(eq nat (s k0 (r k0 i)) (S i)))) with [(Bind _) \Rightarrow (\lambda (i: nat).(refl_equal nat (S i))) | (Flat _) \Rightarrow (\lambda (i: nat).(refl_equal nat (S i)))]).
+
+theorem r_arith0:
+ \forall (k: K).(\forall (i: nat).(eq nat (minus (r k (S i)) (S O)) (r k i)))
+\def
+ \lambda (k: K).(\lambda (i: nat).(eq_ind_r nat (S (r k i)) (\lambda (n: nat).(eq nat (minus n (S O)) (r k i))) (eq_ind_r nat (r k i) (\lambda (n: nat).(eq nat n (r k i))) (refl_equal nat (r k i)) (minus (S (r k i)) (S O)) (minus_Sx_SO (r k i))) (r k (S i)) (r_S k i))).
+
+theorem r_arith1:
+ \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (minus (r k (S i)) (S j)) (minus (r k i) j))))
+\def
+ \lambda (k: K).(\lambda (i: nat).(\lambda (j: nat).(eq_ind_r nat (S (r k i)) (\lambda (n: nat).(eq nat (minus n (S j)) (minus (r k i) j))) (refl_equal nat (minus (r k i) j)) (r k (S i)) (r_S k i)))).
+
+definition tweight:
+ T \to nat
+\def
+ let rec tweight (t: T) on t: nat \def (match t with [(TSort _) \Rightarrow (S O) | (TLRef _) \Rightarrow (S O) | (THead _ u t0) \Rightarrow (S (plus (tweight u) (tweight t0)))]) in tweight.
+
+definition cweight:
+ C \to nat
+\def
+ let rec cweight (c: C) on c: nat \def (match c with [(CSort _) \Rightarrow O | (CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))]) in cweight.
+
+definition clt:
+ C \to (C \to Prop)
+\def
+ \lambda (c1: C).(\lambda (c2: C).(lt (cweight c1) (cweight c2))).
+
+definition cle:
+ C \to (C \to Prop)
+\def
+ \lambda (c1: C).(\lambda (c2: C).(le (cweight c1) (cweight c2))).
+
+theorem tweight_lt:
+ \forall (t: T).(lt O (tweight t))
+\def
+ \lambda (t: T).(match t return (\lambda (t0: T).(lt O (tweight t0))) with [(TSort _) \Rightarrow (le_n (S O)) | (TLRef _) \Rightarrow (le_n (S O)) | (THead _ t0 t1) \Rightarrow (le_S_n (S O) (S (plus (tweight t0) (tweight t1))) (le_n_S (S O) (S (plus (tweight t0) (tweight t1))) (le_n_S O (plus (tweight t0) (tweight t1)) (le_O_n (plus (tweight t0) (tweight t1))))))]).
+
+theorem clt_cong:
+ \forall (c: C).(\forall (d: C).((clt c d) \to (\forall (k: K).(\forall (t: T).(clt (CHead c k t) (CHead d k t))))))
+\def
+ \lambda (c: C).(\lambda (d: C).(\lambda (H: (lt (cweight c) (cweight d))).(\lambda (_: K).(\lambda (t: T).(lt_le_S (plus (cweight c) (tweight t)) (plus (cweight d) (tweight t)) (plus_lt_compat_r (cweight c) (cweight d) (tweight t) H)))))).
+
+theorem clt_head:
+ \forall (k: K).(\forall (c: C).(\forall (u: T).(clt c (CHead c k u))))
+\def
+ \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(eq_ind_r nat (plus (cweight c) O) (\lambda (n: nat).(lt n (plus (cweight c) (tweight u)))) (lt_le_S (plus (cweight c) O) (plus (cweight c) (tweight u)) (plus_le_lt_compat (cweight c) (cweight c) O (tweight u) (le_n (cweight c)) (tweight_lt u))) (cweight c) (plus_n_O (cweight c))))).
+
+theorem clt_wf__q_ind:
+ \forall (P: ((C \to Prop))).(((\forall (n: nat).((\lambda (P: ((C \to Prop))).(\lambda (n0: nat).(\forall (c: C).((eq nat (cweight c) n0) \to (P c))))) P n))) \to (\forall (c: C).(P c)))
+\def
+ let Q \def (\lambda (P: ((C \to Prop))).(\lambda (n: nat).(\forall (c: C).((eq nat (cweight c) n) \to (P c))))) in (\lambda (P: ((C \to Prop))).(\lambda (H: ((\forall (n: nat).(\forall (c: C).((eq nat (cweight c) n) \to (P c)))))).(\lambda (c: C).(H (cweight c) c (refl_equal nat (cweight c)))))).
+
+theorem clt_wf_ind:
+ \forall (P: ((C \to Prop))).(((\forall (c: C).(((\forall (d: C).((clt d c) \to (P d)))) \to (P c)))) \to (\forall (c: C).(P c)))
+\def
+ let Q \def (\lambda (P: ((C \to Prop))).(\lambda (n: nat).(\forall (c: C).((eq nat (cweight c) n) \to (P c))))) in (\lambda (P: ((C \to Prop))).(\lambda (H: ((\forall (c: C).(((\forall (d: C).((lt (cweight d) (cweight c)) \to (P d)))) \to (P c))))).(\lambda (c: C).(clt_wf__q_ind (\lambda (c0: C).(P c0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (c0: C).(P c0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0) \to (Q (\lambda (c: C).(P c)) m))))).(\lambda (c0: C).(\lambda (H1: (eq nat (cweight c0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n: nat).(\forall (m: nat).((lt m n) \to (\forall (c: C).((eq nat (cweight c) m) \to (P c)))))) H0 (cweight c0) H1) in (H c0 (\lambda (d: C).(\lambda (H3: (lt (cweight d) (cweight c0))).(H2 (cweight d) H3 d (refl_equal nat (cweight d))))))))))))) c)))).
+
+definition CTail:
+ K \to (T \to (C \to C))
+\def
+ let rec CTail (k: K) (t: T) (c: C) on c: C \def (match c with [(CSort n) \Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead (CTail k t d) h u)]) in CTail.
+
+theorem chead_ctail:
+ \forall (c: C).(\forall (t: T).(\forall (k: K).(ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c k t) (CTail h u d))))))))
+\def
+ \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (t: T).(\forall (k: K).(ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c0 k t) (CTail h u d))))))))) (\lambda (n: nat).(\lambda (t: T).(\lambda (k: K).(ex_3_intro K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead (CSort n) k t) (CTail h u d))))) k (CSort n) t (refl_equal C (CHead (CSort n) k t)))))) (\lambda (c0: C).(\lambda (H: ((\forall (t: T).(\forall (k: K).(ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c0 k t) (CTail h u d)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (t0: T).(\lambda (k0: K).(let H_x \def (H t k) in (let H0 \def H_x in (ex_3_ind K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c0 k t) (CTail h u d))))) (ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead (CHead c0 k t) k0 t0) (CTail h u d)))))) (\lambda (x0: K).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H1: (eq C (CHead c0 k t) (CTail x0 x2 x1))).(eq_ind_r C (CTail x0 x2 x1) (\lambda (c1: C).(ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c1 k0 t0) (CTail h u d))))))) (ex_3_intro K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead (CTail x0 x2 x1) k0 t0) (CTail h u d))))) x0 (CHead x1 k0 t0) x2 (refl_equal C (CHead (CTail x0 x2 x1) k0 t0))) (CHead c0 k t) H1))))) H0))))))))) c).
+
+theorem clt_thead:
+ \forall (k: K).(\forall (u: T).(\forall (c: C).(clt c (CTail k u c))))
+\def
+ \lambda (k: K).(\lambda (u: T).(\lambda (c: C).(C_ind (\lambda (c0: C).(clt c0 (CTail k u c0))) (\lambda (n: nat).(clt_head k (CSort n) u)) (\lambda (c0: C).(\lambda (H: (clt c0 (CTail k u c0))).(\lambda (k0: K).(\lambda (t: T).(clt_cong c0 (CTail k u c0) H k0 t))))) c))).
+
+theorem c_tail_ind:
+ \forall (P: ((C \to Prop))).(((\forall (n: nat).(P (CSort n)))) \to (((\forall (c: C).((P c) \to (\forall (k: K).(\forall (t: T).(P (CTail k t c))))))) \to (\forall (c: C).(P c))))
+\def
+ \lambda (P: ((C \to Prop))).(\lambda (H: ((\forall (n: nat).(P (CSort n))))).(\lambda (H0: ((\forall (c: C).((P c) \to (\forall (k: K).(\forall (t: T).(P (CTail k t c)))))))).(\lambda (c: C).(clt_wf_ind (\lambda (c0: C).(P c0)) (\lambda (c0: C).(match c0 return (\lambda (c1: C).(((\forall (d: C).((clt d c1) \to (P d)))) \to (P c1))) with [(CSort n) \Rightarrow (\lambda (_: ((\forall (d: C).((clt d (CSort n)) \to (P d))))).(H n)) | (CHead c1 k t) \Rightarrow (\lambda (H1: ((\forall (d: C).((clt d (CHead c1 k t)) \to (P d))))).(let H_x \def (chead_ctail c1 t k) in (let H2 \def H_x in (ex_3_ind K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c1 k t) (CTail h u d))))) (P (CHead c1 k t)) (\lambda (x0: K).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H3: (eq C (CHead c1 k t) (CTail x0 x2 x1))).(eq_ind_r C (CTail x0 x2 x1) (\lambda (c2: C).(P c2)) (let H4 \def (eq_ind C (CHead c1 k t) (\lambda (c: C).(\forall (d: C).((clt d c) \to (P d)))) H1 (CTail x0 x2 x1) H3) in (H0 x1 (H4 x1 (clt_thead x0 x2 x1)) x0 x2)) (CHead c1 k t) H3))))) H2))))])) c)))).
+
+definition fweight:
+ C \to (T \to nat)
+\def
+ \lambda (c: C).(\lambda (t: T).(plus (cweight c) (tweight t))).
+
+definition flt:
+ C \to (T \to (C \to (T \to Prop)))
+\def
+ \lambda (c1: C).(\lambda (t1: T).(\lambda (c2: C).(\lambda (t2: T).(lt (fweight c1 t1) (fweight c2 t2))))).
+
+theorem flt_thead_sx:
+ \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c u c (THead k u t)))))
+\def
+ \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(lt_le_S (plus (cweight c) (tweight u)) (plus (cweight c) (S (plus (tweight u) (tweight t)))) (plus_le_lt_compat (cweight c) (cweight c) (tweight u) (S (plus (tweight u) (tweight t))) (le_n (cweight c)) (le_lt_n_Sm (tweight u) (plus (tweight u) (tweight t)) (le_plus_l (tweight u) (tweight t)))))))).
+
+theorem flt_thead_dx:
+ \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c t c (THead k u t)))))
+\def
+ \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(lt_le_S (plus (cweight c) (tweight t)) (plus (cweight c) (S (plus (tweight u) (tweight t)))) (plus_le_lt_compat (cweight c) (cweight c) (tweight t) (S (plus (tweight u) (tweight t))) (le_n (cweight c)) (le_lt_n_Sm (tweight t) (plus (tweight u) (tweight t)) (le_plus_r (tweight u) (tweight t)))))))).
+
+theorem flt_shift:
+ \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt (CHead c k u) t c (THead k u t)))))
+\def
+ \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(eq_ind nat (S (plus (cweight c) (plus (tweight u) (tweight t)))) (\lambda (n: nat).(lt (plus (plus (cweight c) (tweight u)) (tweight t)) n)) (eq_ind_r nat (plus (plus (cweight c) (tweight u)) (tweight t)) (\lambda (n: nat).(lt (plus (plus (cweight c) (tweight u)) (tweight t)) (S n))) (le_n (S (plus (plus (cweight c) (tweight u)) (tweight t)))) (plus (cweight c) (plus (tweight u) (tweight t))) (plus_assoc (cweight c) (tweight u) (tweight t))) (plus (cweight c) (S (plus (tweight u) (tweight t)))) (plus_n_Sm (cweight c) (plus (tweight u) (tweight t))))))).
+
+theorem flt_arith0:
+ \forall (k: K).(\forall (c: C).(\forall (t: T).(\forall (i: nat).(flt c t (CHead c k t) (TLRef i)))))
+\def
+ \lambda (_: K).(\lambda (c: C).(\lambda (t: T).(\lambda (_: nat).(le_S_n (S (plus (cweight c) (tweight t))) (plus (plus (cweight c) (tweight t)) (S O)) (lt_le_S (S (plus (cweight c) (tweight t))) (S (plus (plus (cweight c) (tweight t)) (S O))) (lt_n_S (plus (cweight c) (tweight t)) (plus (plus (cweight c) (tweight t)) (S O)) (lt_x_plus_x_Sy (plus (cweight c) (tweight t)) O))))))).
+
+theorem flt_arith1:
+ \forall (k1: K).(\forall (c1: C).(\forall (c2: C).(\forall (t1: T).((cle (CHead c1 k1 t1) c2) \to (\forall (k2: K).(\forall (t2: T).(\forall (i: nat).(flt c1 t1 (CHead c2 k2 t2) (TLRef i)))))))))
+\def
+ \lambda (_: K).(\lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda (H: (le (plus (cweight c1) (tweight t1)) (cweight c2))).(\lambda (_: K).(\lambda (t2: T).(\lambda (_: nat).(le_lt_trans (plus (cweight c1) (tweight t1)) (cweight c2) (plus (plus (cweight c2) (tweight t2)) (S O)) H (eq_ind_r nat (plus (S O) (plus (cweight c2) (tweight t2))) (\lambda (n: nat).(lt (cweight c2) n)) (le_lt_n_Sm (cweight c2) (plus (cweight c2) (tweight t2)) (le_plus_l (cweight c2) (tweight t2))) (plus (plus (cweight c2) (tweight t2)) (S O)) (plus_comm (plus (cweight c2) (tweight t2)) (S O))))))))))).
+
+theorem flt_arith2:
+ \forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (i: nat).((flt c1 t1 c2 (TLRef i)) \to (\forall (k2: K).(\forall (t2: T).(\forall (j: nat).(flt c1 t1 (CHead c2 k2 t2) (TLRef j)))))))))
+\def
+ \lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda (_: nat).(\lambda (H: (lt (plus (cweight c1) (tweight t1)) (plus (cweight c2) (S O)))).(\lambda (_: K).(\lambda (t2: T).(\lambda (_: nat).(lt_le_trans (plus (cweight c1) (tweight t1)) (plus (cweight c2) (S O)) (plus (plus (cweight c2) (tweight t2)) (S O)) H (le_S_n (plus (cweight c2) (S O)) (plus (plus (cweight c2) (tweight t2)) (S O)) (lt_le_S (plus (cweight c2) (S O)) (S (plus (plus (cweight c2) (tweight t2)) (S O))) (le_lt_n_Sm (plus (cweight c2) (S O)) (plus (plus (cweight c2) (tweight t2)) (S O)) (plus_le_compat (cweight c2) (plus (cweight c2) (tweight t2)) (S O) (S O) (le_plus_l (cweight c2) (tweight t2)) (le_n (S O)))))))))))))).
+
+theorem flt_wf__q_ind:
+ \forall (P: ((C \to (T \to Prop)))).(((\forall (n: nat).((\lambda (P: ((C \to (T \to Prop)))).(\lambda (n0: nat).(\forall (c: C).(\forall (t: T).((eq nat (fweight c t) n0) \to (P c t)))))) P n))) \to (\forall (c: C).(\forall (t: T).(P c t))))
+\def
+ let Q \def (\lambda (P: ((C \to (T \to Prop)))).(\lambda (n: nat).(\forall (c: C).(\forall (t: T).((eq nat (fweight c t) n) \to (P c t)))))) in (\lambda (P: ((C \to (T \to Prop)))).(\lambda (H: ((\forall (n: nat).(\forall (c: C).(\forall (t: T).((eq nat (fweight c t) n) \to (P c t))))))).(\lambda (c: C).(\lambda (t: T).(H (fweight c t) c t (refl_equal nat (fweight c t))))))).
+
+theorem flt_wf_ind:
+ \forall (P: ((C \to (T \to Prop)))).(((\forall (c2: C).(\forall (t2: T).(((\forall (c1: C).(\forall (t1: T).((flt c1 t1 c2 t2) \to (P c1 t1))))) \to (P c2 t2))))) \to (\forall (c: C).(\forall (t: T).(P c t))))
+\def
+ let Q \def (\lambda (P: ((C \to (T \to Prop)))).(\lambda (n: nat).(\forall (c: C).(\forall (t: T).((eq nat (fweight c t) n) \to (P c t)))))) in (\lambda (P: ((C \to (T \to Prop)))).(\lambda (H: ((\forall (c2: C).(\forall (t2: T).(((\forall (c1: C).(\forall (t1: T).((flt c1 t1 c2 t2) \to (P c1 t1))))) \to (P c2 t2)))))).(\lambda (c: C).(\lambda (t: T).(flt_wf__q_ind P (\lambda (n: nat).(lt_wf_ind n (Q P) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0) \to (Q P m))))).(\lambda (c0: C).(\lambda (t0: T).(\lambda (H1: (eq nat (fweight c0 t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n: nat).(\forall (m: nat).((lt m n) \to (\forall (c: C).(\forall (t: T).((eq nat (fweight c t) m) \to (P c t))))))) H0 (fweight c0 t0) H1) in (H c0 t0 (\lambda (c1: C).(\lambda (t1: T).(\lambda (H3: (flt c1 t1 c0 t0)).(H2 (fweight c1 t1) H3 c1 t1 (refl_equal nat (fweight c1 t1))))))))))))))) c t))))).
+
+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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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 (_: ?).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 (_: ?).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 (_: ?).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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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) 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) 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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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) 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) 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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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 (_: ?).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).((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) 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) 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 (_: ?).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 (_: ?).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 (_: ?).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 (_: ?).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) 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) 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).((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 (_: ?).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 (_: ?).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)))))).