n) O u0)) (ty3 g c t3 (lift (S n) O t0)) (\lambda (H6: (eq nat n i)).(\lambda
(H7: (eq T t3 (lift (S n) O u0))).(eq_ind_r T (lift (S n) O u0) (\lambda (t4:
T).(ty3 g c t4 (lift (S n) O t0))) (let H8 \def (eq_ind_r nat i (\lambda (n0:
n) O u0)) (ty3 g c t3 (lift (S n) O t0)) (\lambda (H6: (eq nat n i)).(\lambda
(H7: (eq T t3 (lift (S n) O u0))).(eq_ind_r T (lift (S n) O u0) (\lambda (t4:
T).(ty3 g c t4 (lift (S n) O t0))) (let H8 \def (eq_ind_r nat i (\lambda (n0: