+i d0 (le_S_n i d0 (le_S_n (S i) (S d0) (le_S (S (S i)) (S d0) (le_n_S (S i)
+d0 H4)))) c0 c h H3 (CHead d (Bind Abbr) v) H0) in (ex3_2_ind C C (\lambda
+(e0: C).(\lambda (_: C).(drop i O c0 e0))) (\lambda (e0: C).(\lambda (e1:
+C).(drop h (minus d0 i) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1
+(CHead d (Bind Abbr) v)))) (sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift
+(S i) O w))) (\lambda (x0: C).(\lambda (x1: C).(\lambda (H6: (drop i O c0
+x0)).(\lambda (H7: (drop h (minus d0 i) x0 x1)).(\lambda (H8: (clear x1
+(CHead d (Bind Abbr) v))).(let H9 \def (eq_ind nat (minus d0 i) (\lambda (n:
+nat).(drop h n x0 x1)) H7 (S (minus d0 (S i))) (minus_x_Sy d0 i H4)) in (let
+H10 \def (drop_clear_S x1 x0 h (minus d0 (S i)) H9 Abbr d v H8) in (ex2_ind C
+(\lambda (c1: C).(clear x0 (CHead c1 (Bind Abbr) (lift h (minus d0 (S i))
+v)))) (\lambda (c1: C).(drop h (minus d0 (S i)) c1 d)) (sty0 g c0 (lift h d0
+(TLRef i)) (lift h d0 (lift (S i) O w))) (\lambda (x: C).(\lambda (H11:
+(clear x0 (CHead x (Bind Abbr) (lift h (minus d0 (S i)) v)))).(\lambda (H12:
+(drop h (minus d0 (S i)) x d)).(eq_ind_r T (TLRef i) (\lambda (t: T).(sty0 g
+c0 t (lift h d0 (lift (S i) O w)))) (eq_ind nat (plus (S i) (minus d0 (S i)))
+(\lambda (n: nat).(sty0 g c0 (TLRef i) (lift h n (lift (S i) O w))))
+(eq_ind_r T (lift (S i) O (lift h (minus d0 (S i)) w)) (\lambda (t: T).(sty0
+g c0 (TLRef i) t)) (eq_ind nat d0 (\lambda (_: nat).(sty0 g c0 (TLRef i)
+(lift (S i) O (lift h (minus d0 (S i)) w)))) (sty0_abbr g c0 x (lift h (minus
+d0 (S i)) v) i (getl_intro i c0 (CHead x (Bind Abbr) (lift h (minus d0 (S i))
+v)) x0 H6 H11) (lift h (minus d0 (S i)) w) (H2 x h (minus d0 (S i)) H12))
+(plus (S i) (minus d0 (S i))) (le_plus_minus (S i) d0 H4)) (lift h (plus (S
+i) (minus d0 (S i))) (lift (S i) O w)) (lift_d w h (S i) (minus d0 (S i)) O
+(le_O_n (minus d0 (S i))))) d0 (le_plus_minus_r (S i) d0 H4)) (lift h d0
+(TLRef i)) (lift_lref_lt i h d0 H4))))) H10)))))))) H5))) (\lambda (H4: (le
+d0 i)).(eq_ind_r T (TLRef (plus i h)) (\lambda (t: T).(sty0 g c0 t (lift h d0
+(lift (S i) O w)))) (eq_ind nat (S i) (\lambda (_: nat).(sty0 g c0 (TLRef
+(plus i h)) (lift h d0 (lift (S i) O w)))) (eq_ind_r T (lift (plus h (S i)) O
+w) (\lambda (t: T).(sty0 g c0 (TLRef (plus i h)) t)) (eq_ind_r nat (plus (S
+i) h) (\lambda (n: nat).(sty0 g c0 (TLRef (plus i h)) (lift n O w)))
+(sty0_abbr g c0 d v (plus i h) (drop_getl_trans_ge i c0 c d0 h H3 (CHead d
+(Bind Abbr) v) H0 H4) w H1) (plus h (S i)) (plus_sym h (S i))) (lift h d0
+(lift (S i) O w)) (lift_free w (S i) h O d0 (le_S_n d0 (S i) (le_S (S d0) (S
+i) (le_n_S d0 i H4))) (le_O_n d0))) (plus i (S O)) (eq_ind_r nat (plus (S O)
+i) (\lambda (n: nat).(eq nat (S i) n)) (le_antisym (S i) (plus (S O) i) (le_n
+(plus (S O) i)) (le_n (S i))) (plus i (S O)) (plus_sym i (S O)))) (lift h d0
+(TLRef i)) (lift_lref_ge i h d0 H4)))))))))))))))) (\lambda (c: C).(\lambda
+(d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d
+(Bind Abst) v))).(\lambda (w: T).(\lambda (H1: (sty0 g d v w)).(\lambda (H2:
+((\forall (c0: C).(\forall (h: nat).(\forall (d0: nat).((drop h d0 c0 d) \to
+(sty0 g c0 (lift h d0 v) (lift h d0 w)))))))).(\lambda (c0: C).(\lambda (h:
+nat).(\lambda (d0: nat).(\lambda (H3: (drop h d0 c0 c)).(lt_le_e i d0 (sty0 g
+c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))) (\lambda (H4: (lt i
+d0)).(let H5 \def (drop_getl_trans_le i d0 (le_S_n i d0 (le_S_n (S i) (S d0)
+(le_S (S (S i)) (S d0) (le_n_S (S i) d0 H4)))) c0 c h H3 (CHead d (Bind Abst)
+v) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop i O c0 e0)))