-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