(\lambda (H3: (eq nat n i)).(\lambda (_: (eq T x (lift (S n) O u))).(let H5
\def (eq_ind nat n (\lambda (n0: nat).(lt n0 d)) H1 i H3) in (le_false (plus
d h) i (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2:
T).(subst0 (minus i h) u (TLRef n) t2))) H0 (le_plus_trans (S i) d h H5)))))
(subst0_gen_lref u x i n H2)))) (\lambda (H1: (le d n)).(let H2 \def (eq_ind
T (lift h d (TLRef n)) (\lambda (t: T).(subst0 i u t x)) H (TLRef (plus n h))
(\lambda (H3: (eq nat n i)).(\lambda (_: (eq T x (lift (S n) O u))).(let H5
\def (eq_ind nat n (\lambda (n0: nat).(lt n0 d)) H1 i H3) in (le_false (plus
d h) i (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2:
T).(subst0 (minus i h) u (TLRef n) t2))) H0 (le_plus_trans (S i) d h H5)))))
(subst0_gen_lref u x i n H2)))) (\lambda (H1: (le d n)).(let H2 \def (eq_ind
T (lift h d (TLRef n)) (\lambda (t: T).(subst0 i u t x)) H (TLRef (plus n h))