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))
+(plus n h)) (eq T (TLRef n) (TLRef n)) (le_plus_plus 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
d)).(\lambda (t: T).(\lambda (H0: (eq T (TLRef n) (lift h d t))).(let H_x
\def (lift_gen_lref t d h n H0) in (let H1 \def H_x in (or_ind (land (lt n d)
(eq T t (TLRef n))) (land (le (plus d h) n) (eq T t (TLRef (minus n h)))) (eq
-T t (TLRef n)) (\lambda (H2: (land (lt n d) (eq T t (TLRef n)))).(and_ind (lt
-n d) (eq T t (TLRef n)) (eq T t (TLRef n)) (\lambda (_: (lt n d)).(\lambda
-(H4: (eq T t (TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0
-(TLRef n))) (refl_equal T (TLRef n)) t H4))) H2)) (\lambda (H2: (land (le
-(plus d h) n) (eq T t (TLRef (minus n h))))).(and_ind (le (plus d h) n) (eq T
-t (TLRef (minus n h))) (eq T t (TLRef n)) (\lambda (H3: (le (plus d h)
-n)).(\lambda (H4: (eq T t (TLRef (minus n h)))).(eq_ind_r T (TLRef (minus n
-h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false (plus d h) n (eq T (TLRef
-(minus n h)) (TLRef n)) H3 (lt_le_S n (plus d h) (le_plus_trans (S n) d h
-H))) t H4))) H2)) H1)))))))).
+T t (TLRef n)) (\lambda (H2: (land (lt n d) (eq T t (TLRef n)))).(land_ind
+(lt n d) (eq T t (TLRef n)) (eq T t (TLRef n)) (\lambda (_: (lt n
+d)).(\lambda (H4: (eq T t (TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0:
+T).(eq T t0 (TLRef n))) (refl_equal T (TLRef n)) t H4))) H2)) (\lambda (H2:
+(land (le (plus d h) n) (eq T t (TLRef (minus n h))))).(land_ind (le (plus d
+h) n) (eq T t (TLRef (minus n h))) (eq T t (TLRef n)) (\lambda (H3: (le (plus
+d h) n)).(\lambda (H4: (eq T t (TLRef (minus n h)))).(eq_ind_r T (TLRef
+(minus n h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false (plus d h) n (eq
+T (TLRef (minus n h)) (TLRef n)) H3 (lt_le_S n (plus d h) (le_plus_trans (S
+n) d h H))) t H4))) H2)) H1)))))))).
theorem lift_gen_lref_false:
\forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to ((lt n
(TLRef n) (lift h d t))).(\lambda (P: Prop).(let H_x \def (lift_gen_lref t d
h n H1) in (let H2 \def H_x in (or_ind (land (lt n d) (eq T t (TLRef n)))
(land (le (plus d h) n) (eq T t (TLRef (minus n h)))) P (\lambda (H3: (land
-(lt n d) (eq T t (TLRef n)))).(and_ind (lt n d) (eq T t (TLRef n)) P (\lambda
-(H4: (lt n d)).(\lambda (_: (eq T t (TLRef n))).(le_false d n P H H4))) H3))
-(\lambda (H3: (land (le (plus d h) n) (eq T t (TLRef (minus n h))))).(and_ind
-(le (plus d h) n) (eq T t (TLRef (minus n h))) P (\lambda (H4: (le (plus d h)
-n)).(\lambda (_: (eq T t (TLRef (minus n h)))).(le_false (plus d h) n P H4
-H0))) H3)) H2)))))))))).
+(lt n d) (eq T t (TLRef n)))).(land_ind (lt n d) (eq T t (TLRef n)) P
+(\lambda (H4: (lt n d)).(\lambda (_: (eq T t (TLRef n))).(le_false d n P H
+H4))) H3)) (\lambda (H3: (land (le (plus d h) n) (eq T t (TLRef (minus n
+h))))).(land_ind (le (plus d h) n) (eq T t (TLRef (minus n h))) P (\lambda
+(H4: (le (plus d h) n)).(\lambda (_: (eq T t (TLRef (minus n h)))).(le_false
+(plus d h) n P H4 H0))) H3)) H2)))))))))).
theorem lift_gen_lref_ge:
\forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to (\forall
t))).(let H_x \def (lift_gen_lref t d h (plus n h) H0) in (let H1 \def H_x in
(or_ind (land (lt (plus n h) d) (eq T t (TLRef (plus n h)))) (land (le (plus
d h) (plus n h)) (eq T t (TLRef (minus (plus n h) h)))) (eq T t (TLRef n))
-(\lambda (H2: (land (lt (plus n h) d) (eq T t (TLRef (plus n h))))).(and_ind
+(\lambda (H2: (land (lt (plus n h) d) (eq T t (TLRef (plus n h))))).(land_ind
(lt (plus n h) d) (eq T t (TLRef (plus n h))) (eq T t (TLRef n)) (\lambda
(H3: (lt (plus n h) d)).(\lambda (H4: (eq T t (TLRef (plus n h)))).(eq_ind_r
T (TLRef (plus n h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false d n (eq
T (TLRef (plus n h)) (TLRef n)) H (lt_le_S n d (simpl_lt_plus_r h n d
(lt_le_trans (plus n h) d (plus d h) H3 (le_plus_l d h))))) t H4))) H2))
(\lambda (H2: (land (le (plus d h) (plus n h)) (eq T t (TLRef (minus (plus n
-h) h))))).(and_ind (le (plus d h) (plus n h)) (eq T t (TLRef (minus (plus n
+h) h))))).(land_ind (le (plus d h) (plus n h)) (eq T t (TLRef (minus (plus n
h) h))) (eq T t (TLRef n)) (\lambda (_: (le (plus d h) (plus n h))).(\lambda
(H4: (eq T t (TLRef (minus (plus n h) h)))).(eq_ind_r T (TLRef (minus (plus n
h) h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (f_equal nat T TLRef (minus
x))).(let H_x \def (lift_gen_head (Bind b) u t x h d H) in (let H0 \def H_x
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 u (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T t (lift h (s (Bind b) d) z)))) (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))))) (\lambda (x0: T).(\lambda (x1: T).(\lambda
-(H1: (eq T x (THead (Bind b) x0 x1))).(\lambda (H2: (eq T u (lift h d
-x0))).(\lambda (H3: (eq T t (lift h (s (Bind b) d) x1))).(eq_ind_r T (THead
-(Bind b) x0 x1) (\lambda (t0: T).(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))))))
-(eq_ind_r T (lift h (s (Bind b) d) x1) (\lambda (t0: T).(ex3_2 T T (\lambda
-(y: T).(\lambda (z: T).(eq T (THead (Bind b) x0 x1) (THead (Bind b) y z))))
-(\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T t0 (lift h (S d) z)))))) (eq_ind_r T (lift h d x0)
-(\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead
+T).(\lambda (z: T).(eq T t (lift h (S d) z)))) (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))))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T x (THead
+(Bind b) x0 x1))).(\lambda (H2: (eq T u (lift h d x0))).(\lambda (H3: (eq T t
+(lift h (S d) x1))).(eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t0:
+T).(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)))))) (eq_ind_r T (lift h (S d)
+x1) (\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead
(Bind b) x0 x1) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T
-t0 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s (Bind b)
-d) x1) (lift h (S d) z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z:
-T).(eq T (THead (Bind b) x0 x1) (THead (Bind b) y z)))) (\lambda (y:
-T).(\lambda (_: T).(eq T (lift h d x0) (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T (lift h (s (Bind b) d) x1) (lift h (S d) z)))) x0 x1
-(refl_equal T (THead (Bind b) x0 x1)) (refl_equal T (lift h d x0))
-(refl_equal T (lift h (S d) x1))) u H2) t H3) x H1)))))) H0))))))))).
+u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t0 (lift h (S d)
+z)))))) (eq_ind_r T (lift h d x0) (\lambda (t0: T).(ex3_2 T T (\lambda (y:
+T).(\lambda (z: T).(eq T (THead (Bind b) x0 x1) (THead (Bind b) y z))))
+(\lambda (y: T).(\lambda (_: T).(eq T t0 (lift h d y)))) (\lambda (_:
+T).(\lambda (z: T).(eq T (lift h (S d) x1) (lift h (S d) z)))))) (ex3_2_intro
+T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Bind b) x0 x1) (THead (Bind
+b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d x0) (lift h d
+y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (S d) x1) (lift h (S d)
+z)))) x0 x1 (refl_equal T (THead (Bind b) x0 x1)) (refl_equal T (lift h d
+x0)) (refl_equal T (lift h (S d) x1))) u H2) t H3) x H1)))))) H0))))))))).
theorem lift_gen_flat:
\forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
x))).(let H_x \def (lift_gen_head (Flat f) u t x h d H) in (let H0 \def H_x
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 u (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T t (lift h (s (Flat f) d) z)))) (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))))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1:
-(eq T x (THead (Flat f) x0 x1))).(\lambda (H2: (eq T u (lift h d
-x0))).(\lambda (H3: (eq T t (lift h (s (Flat f) d) x1))).(eq_ind_r T (THead
-(Flat f) x0 x1) (\lambda (t0: T).(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))))))
-(eq_ind_r T (lift h (s (Flat f) d) x1) (\lambda (t0: T).(ex3_2 T T (\lambda
-(y: T).(\lambda (z: T).(eq T (THead (Flat f) x0 x1) (THead (Flat f) y z))))
-(\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T t0 (lift h d z)))))) (eq_ind_r T (lift h d x0)
-(\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead
-(Flat f) x0 x1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T
-t0 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s (Flat f)
-d) x1) (lift h d z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq
+T).(\lambda (z: T).(eq T t (lift h d z)))) (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))))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T x (THead
+(Flat f) x0 x1))).(\lambda (H2: (eq T u (lift h d x0))).(\lambda (H3: (eq T t
+(lift h d x1))).(eq_ind_r T (THead (Flat f) x0 x1) (\lambda (t0: T).(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)))))) (eq_ind_r T (lift h d x1) (\lambda (t0:
+T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Flat f) x0 x1)
+(THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d
+y)))) (\lambda (_: T).(\lambda (z: T).(eq T t0 (lift h d z)))))) (eq_ind_r T
+(lift h d x0) (\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq
T (THead (Flat f) x0 x1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_:
+T).(eq T t0 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h d
+x1) (lift h d z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T
+(THead (Flat f) x0 x1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_:
T).(eq T (lift h d x0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T
-(lift h (s (Flat f) d) x1) (lift h d z)))) x0 x1 (refl_equal T (THead (Flat
-f) x0 x1)) (refl_equal T (lift h d x0)) (refl_equal T (lift h d x1))) u H2) t
-H3) x H1)))))) H0))))))))).
+(lift h d x1) (lift h d z)))) x0 x1 (refl_equal T (THead (Flat f) x0 x1))
+(refl_equal T (lift h d x0)) (refl_equal T (lift h d x1))) u H2) t H3) x
+H1)))))) H0))))))))).