-(lift h d t0) (lift h d t3)))))))).(\lambda (t4: T).(\lambda (_: (ty3 g
-(CHead c (Bind b) u) t3 t4)).(\lambda (H5: ((\forall (c0: C).(\forall (d:
-nat).(\forall (h: nat).((drop h d c0 (CHead c (Bind b) u)) \to (ty3 g c0
-(lift h d t3) (lift h d t4)))))))).(\lambda (c0: C).(\lambda (d:
-nat).(\lambda (h: nat).(\lambda (H6: (drop h d c0 c)).(eq_ind_r T (THead
-(Bind b) (lift h d u) (lift h (s (Bind b) d) t0)) (\lambda (t5: T).(ty3 g c0
-t5 (lift h d (THead (Bind b) u t3)))) (eq_ind_r T (THead (Bind b) (lift h d
-u) (lift h (s (Bind b) d) t3)) (\lambda (t5: T).(ty3 g c0 (THead (Bind b)
-(lift h d u) (lift h (s (Bind b) d) t0)) t5)) (ty3_bind g c0 (lift h d u)
-(lift h d t) (H1 c0 d h H6) b (lift h (S d) t0) (lift h (S d) t3) (H3 (CHead
-c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0 c H6 b u)) (lift h
-(S d) t4) (H5 (CHead c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0
-c H6 b u))) (lift h d (THead (Bind b) u t3)) (lift_head (Bind b) u t3 h d))
-(lift h d (THead (Bind b) u t0)) (lift_head (Bind b) u t0 h
-d))))))))))))))))))) (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda
-(_: (ty3 g c w u)).(\lambda (H1: ((\forall (c0: C).(\forall (d: nat).(\forall
-(h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d w) (lift h d
-u)))))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead
-(Bind Abst) u t))).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall
-(h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d v) (lift h d (THead (Bind
-Abst) u t))))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h:
-nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead (Flat Appl) (lift h d
-w) (lift h (s (Flat Appl) d) v)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d
-(THead (Flat Appl) w (THead (Bind Abst) u t))))) (eq_ind_r T (THead (Flat
-Appl) (lift h d w) (lift h (s (Flat Appl) d) (THead (Bind Abst) u t)))
-(\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) (lift h d w) (lift h (s (Flat
-Appl) d) v)) t0)) (eq_ind_r T (THead (Bind Abst) (lift h (s (Flat Appl) d) u)
-(lift h (s (Bind Abst) (s (Flat Appl) d)) t)) (\lambda (t0: T).(ty3 g c0
-(THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) (THead (Flat
-Appl) (lift h d w) t0))) (ty3_appl g c0 (lift h d w) (lift h d u) (H1 c0 d h
-H4) (lift h d v) (lift h (S d) t) (eq_ind T (lift h d (THead (Bind Abst) u
-t)) (\lambda (t0: T).(ty3 g c0 (lift h d v) t0)) (H3 c0 d h H4) (THead (Bind
-Abst) (lift h d u) (lift h (S d) t)) (lift_bind Abst u t h d))) (lift h (s
-(Flat Appl) d) (THead (Bind Abst) u t)) (lift_head (Bind Abst) u t h (s (Flat
-Appl) d))) (lift h d (THead (Flat Appl) w (THead (Bind Abst) u t)))
-(lift_head (Flat Appl) w (THead (Bind Abst) u t) h d)) (lift h d (THead (Flat
-Appl) w v)) (lift_head (Flat Appl) w v h d))))))))))))))) (\lambda (c:
-C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g c t0 t3)).(\lambda
-(H1: ((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c)
-\to (ty3 g c0 (lift h d t0) (lift h d t3)))))))).(\lambda (t4: T).(\lambda
-(_: (ty3 g c t3 t4)).(\lambda (H3: ((\forall (c0: C).(\forall (d:
-nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t3) (lift h d
-t4)))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4:
-(drop h d c0 c)).(eq_ind_r T (THead (Flat Cast) (lift h d t3) (lift h (s
-(Flat Cast) d) t0)) (\lambda (t: T).(ty3 g c0 t (lift h d (THead (Flat Cast)
-t4 t3)))) (eq_ind_r T (THead (Flat Cast) (lift h d t4) (lift h (s (Flat Cast)
-d) t3)) (\lambda (t: T).(ty3 g c0 (THead (Flat Cast) (lift h d t3) (lift h (s
-(Flat Cast) d) t0)) t)) (ty3_cast g c0 (lift h (s (Flat Cast) d) t0) (lift h
-(s (Flat Cast) d) t3) (H1 c0 (s (Flat Cast) d) h H4) (lift h d t4) (H3 c0 d h
-H4)) (lift h d (THead (Flat Cast) t4 t3)) (lift_head (Flat Cast) t4 t3 h d))
-(lift h d (THead (Flat Cast) t3 t0)) (lift_head (Flat Cast) t3 t0 h
-d)))))))))))))) e t1 t2 H))))).
+(lift h d t0) (lift h d t3)))))))).(\lambda (c0: C).(\lambda (d:
+nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead
+(Bind b) (lift h d u) (lift h (s (Bind b) d) t0)) (\lambda (t4: T).(ty3 g c0
+t4 (lift h d (THead (Bind b) u t3)))) (eq_ind_r T (THead (Bind b) (lift h d
+u) (lift h (s (Bind b) d) t3)) (\lambda (t4: T).(ty3 g c0 (THead (Bind b)
+(lift h d u) (lift h (s (Bind b) d) t0)) t4)) (ty3_bind g c0 (lift h d u)
+(lift h d t) (H1 c0 d h H4) b (lift h (S d) t0) (lift h (S d) t3) (H3 (CHead
+c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0 c H4 b u))) (lift h
+d (THead (Bind b) u t3)) (lift_head (Bind b) u t3 h d)) (lift h d (THead
+(Bind b) u t0)) (lift_head (Bind b) u t0 h d)))))))))))))))) (\lambda (c:
+C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w u)).(\lambda (H1:
+((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
+(ty3 g c0 (lift h d w) (lift h d u)))))))).(\lambda (v: T).(\lambda (t:
+T).(\lambda (_: (ty3 g c v (THead (Bind Abst) u t))).(\lambda (H3: ((\forall
+(c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0
+(lift h d v) (lift h d (THead (Bind Abst) u t))))))))).(\lambda (c0:
+C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0
+c)).(eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v))
+(\lambda (t0: T).(ty3 g c0 t0 (lift h d (THead (Flat Appl) w (THead (Bind
+Abst) u t))))) (eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat
+Appl) d) (THead (Bind Abst) u t))) (\lambda (t0: T).(ty3 g c0 (THead (Flat
+Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) t0)) (eq_ind_r T (THead
+(Bind Abst) (lift h (s (Flat Appl) d) u) (lift h (s (Bind Abst) (s (Flat
+Appl) d)) t)) (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) (lift h d w)
+(lift h (s (Flat Appl) d) v)) (THead (Flat Appl) (lift h d w) t0))) (ty3_appl
+g c0 (lift h d w) (lift h d u) (H1 c0 d h H4) (lift h d v) (lift h (S d) t)
+(eq_ind T (lift h d (THead (Bind Abst) u t)) (\lambda (t0: T).(ty3 g c0 (lift
+h d v) t0)) (H3 c0 d h H4) (THead (Bind Abst) (lift h d u) (lift h (S d) t))
+(lift_bind Abst u t h d))) (lift h (s (Flat Appl) d) (THead (Bind Abst) u t))
+(lift_head (Bind Abst) u t h (s (Flat Appl) d))) (lift h d (THead (Flat Appl)
+w (THead (Bind Abst) u t))) (lift_head (Flat Appl) w (THead (Bind Abst) u t)
+h d)) (lift h d (THead (Flat Appl) w v)) (lift_head (Flat Appl) w v h
+d))))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda
+(_: (ty3 g c t0 t3)).(\lambda (H1: ((\forall (c0: C).(\forall (d:
+nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t0) (lift h d
+t3)))))))).(\lambda (t4: T).(\lambda (_: (ty3 g c t3 t4)).(\lambda (H3:
+((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
+(ty3 g c0 (lift h d t3) (lift h d t4)))))))).(\lambda (c0: C).(\lambda (d:
+nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead
+(Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)) (\lambda (t: T).(ty3
+g c0 t (lift h d (THead (Flat Cast) t4 t3)))) (eq_ind_r T (THead (Flat Cast)
+(lift h d t4) (lift h (s (Flat Cast) d) t3)) (\lambda (t: T).(ty3 g c0 (THead
+(Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)) t)) (ty3_cast g c0
+(lift h (s (Flat Cast) d) t0) (lift h (s (Flat Cast) d) t3) (H1 c0 (s (Flat
+Cast) d) h H4) (lift h d t4) (H3 c0 d h H4)) (lift h d (THead (Flat Cast) t4
+t3)) (lift_head (Flat Cast) t4 t3 h d)) (lift h d (THead (Flat Cast) t3 t0))
+(lift_head (Flat Cast) t3 t0 h d)))))))))))))) e t1 t2 H))))).