-(lift h d' t3) (lift h d' w))) (subst0_lift_lt t3 w u2 O H4 (S d) (lt_le_S O
-(S d) (le_lt_n_Sm O d (le_O_n d))) h) d (eq_ind nat d (\lambda (n: nat).(eq
-nat n d)) (refl_equal nat d) (minus d O) (minus_n_O d))))) (lift h d (THead
-(Bind Abbr) u2 w)) (lift_head (Bind Abbr) u2 w h d)) (lift h d (THead (Bind
-Abbr) u1 t0)) (lift_head (Bind Abbr) u1 t0 h d)))))))))))))) (\lambda (b:
-B).(\lambda (H0: (not (eq B b Abst))).(\lambda (t0: T).(\lambda (t3:
-T).(\lambda (_: (pr0 t0 t3)).(\lambda (H2: ((\forall (h: nat).(\forall (d:
-nat).(pr0 (lift h d t0) (lift h d t3)))))).(\lambda (u: T).(\lambda (h:
-nat).(\lambda (d: nat).(eq_ind_r T (THead (Bind b) (lift h d u) (lift h (s
-(Bind b) d) (lift (S O) O t0))) (\lambda (t: T).(pr0 t (lift h d t3)))
-(eq_ind nat (plus (S O) d) (\lambda (n: nat).(pr0 (THead (Bind b) (lift h d
-u) (lift h n (lift (S O) O t0))) (lift h d t3))) (eq_ind_r T (lift (S O) O
-(lift h d t0)) (\lambda (t: T).(pr0 (THead (Bind b) (lift h d u) t) (lift h d
-t3))) (pr0_zeta b H0 (lift h d t0) (lift h d t3) (H2 h d) (lift h d u)) (lift
-h (plus (S O) d) (lift (S O) O t0)) (lift_d t0 h (S O) d O (le_O_n d))) (S d)
-(refl_equal nat (S d))) (lift h d (THead (Bind b) u (lift (S O) O t0)))
-(lift_head (Bind b) u (lift (S O) O t0) h d))))))))))) (\lambda (t0:
-T).(\lambda (t3: T).(\lambda (_: (pr0 t0 t3)).(\lambda (H1: ((\forall (h:
-nat).(\forall (d: nat).(pr0 (lift h d t0) (lift h d t3)))))).(\lambda (u:
-T).(\lambda (h: nat).(\lambda (d: nat).(eq_ind_r T (THead (Flat Cast) (lift h
-d u) (lift h (s (Flat Cast) d) t0)) (\lambda (t: T).(pr0 t (lift h d t3)))
-(pr0_epsilon (lift h (s (Flat Cast) d) t0) (lift h d t3) (H1 h d) (lift h d
-u)) (lift h d (THead (Flat Cast) u t0)) (lift_head (Flat Cast) u t0 h
-d))))))))) t1 t2 H))).
+(lift h d' t3) (lift h d' w))) (subst0_lift_lt t3 w u2 O H4 (S d) (le_n_S O d
+(le_O_n d)) h) d (eq_ind nat d (\lambda (n: nat).(eq nat n d)) (refl_equal
+nat d) (minus d O) (minus_n_O d))))) (lift h d (THead (Bind Abbr) u2 w))
+(lift_head (Bind Abbr) u2 w h d)) (lift h d (THead (Bind Abbr) u1 t0))
+(lift_head (Bind Abbr) u1 t0 h d)))))))))))))) (\lambda (b: B).(\lambda (H0:
+(not (eq B b Abst))).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (pr0 t0
+t3)).(\lambda (H2: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t0)
+(lift h d t3)))))).(\lambda (u: T).(\lambda (h: nat).(\lambda (d:
+nat).(eq_ind_r T (THead (Bind b) (lift h d u) (lift h (s (Bind b) d) (lift (S
+O) O t0))) (\lambda (t: T).(pr0 t (lift h d t3))) (eq_ind nat (plus (S O) d)
+(\lambda (n: nat).(pr0 (THead (Bind b) (lift h d u) (lift h n (lift (S O) O
+t0))) (lift h d t3))) (eq_ind_r T (lift (S O) O (lift h d t0)) (\lambda (t:
+T).(pr0 (THead (Bind b) (lift h d u) t) (lift h d t3))) (pr0_zeta b H0 (lift
+h d t0) (lift h d t3) (H2 h d) (lift h d u)) (lift h (plus (S O) d) (lift (S
+O) O t0)) (lift_d t0 h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S d)))
+(lift h d (THead (Bind b) u (lift (S O) O t0))) (lift_head (Bind b) u (lift
+(S O) O t0) h d))))))))))) (\lambda (t0: T).(\lambda (t3: T).(\lambda (_:
+(pr0 t0 t3)).(\lambda (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h
+d t0) (lift h d t3)))))).(\lambda (u: T).(\lambda (h: nat).(\lambda (d:
+nat).(eq_ind_r T (THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d)
+t0)) (\lambda (t: T).(pr0 t (lift h d t3))) (pr0_epsilon (lift h (s (Flat
+Cast) d) t0) (lift h d t3) (H1 h d) (lift h d u)) (lift h d (THead (Flat
+Cast) u t0)) (lift_head (Flat Cast) u t0 h d))))))))) t1 t2 H))).