(\lambda (t0: T).(eq T t0 (lift h d t))) (refl_equal T (lift h d t)) (\lambda
(t2: T).(\lambda (H2: (subst0 i u (lift h d t) t2)).(subst0_gen_lift_false t
u t2 h d i H H0 H2 (eq T t2 (lift h d t))))) x H1))))))))).
(\lambda (t0: T).(eq T t0 (lift h d t))) (refl_equal T (lift h d t)) (\lambda
(t2: T).(\lambda (H2: (subst0 i u (lift h d t) t2)).(subst0_gen_lift_false t
u t2 h d i H H0 H2 (eq T t2 (lift h d t))))) x H1))))))))).