(eq_ind_r nat (plus (trans hds0 i) h) (\lambda (n: nat).(eq T (lift (S n) O
(lift1 (ptrans hds0 i) t)) (lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans
hds0 i) t)))) (refl_equal T (lift (S (plus (trans hds0 i) h)) O (lift1
(eq_ind_r nat (plus (trans hds0 i) h) (\lambda (n: nat).(eq T (lift (S n) O
(lift1 (ptrans hds0 i) t)) (lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans
hds0 i) t)))) (refl_equal T (lift (S (plus (trans hds0 i) h)) O (lift1
(plus h (S (trans hds0 i))) (plus_n_Sm h (trans hds0 i))) (lift h d (lift (S
(trans hds0 i)) O (lift1 (ptrans hds0 i) t))) (lift_free (lift1 (ptrans hds0
i) t) (S (trans hds0 i)) h O d (eq_ind nat (S (plus O (trans hds0 i)))
(\lambda (n: nat).(le d n)) (eq_ind_r nat (plus (trans hds0 i) O) (\lambda
(n: nat).(le d (S n))) (le_S d (plus (trans hds0 i) O) (le_plus_trans d
(trans hds0 i) O (bge_le d (trans hds0 i) H0))) (plus O (trans hds0 i))
(plus h (S (trans hds0 i))) (plus_n_Sm h (trans hds0 i))) (lift h d (lift (S
(trans hds0 i)) O (lift1 (ptrans hds0 i) t))) (lift_free (lift1 (ptrans hds0
i) t) (S (trans hds0 i)) h O d (eq_ind nat (S (plus O (trans hds0 i)))
(\lambda (n: nat).(le d n)) (eq_ind_r nat (plus (trans hds0 i) O) (\lambda
(n: nat).(le d (S n))) (le_S d (plus (trans hds0 i) O) (le_plus_trans d
(trans hds0 i) O (bge_le d (trans hds0 i) H0))) (plus O (trans hds0 i))