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))))))))).