(trans p i) | false \Rightarrow (plus (trans p i) n)])))) (refl_equal T
(TLRef (match (blt (trans p i) n0) with [true \Rightarrow (trans p i) | false
\Rightarrow (plus (trans p i) n)]))) (lift1 p (TLRef i)) (H i))))))) hds).
(trans p i) | false \Rightarrow (plus (trans p i) n)])))) (refl_equal T
(TLRef (match (blt (trans p i) n0) with [true \Rightarrow (trans p i) | false
\Rightarrow (plus (trans p i) n)]))) (lift1 p (TLRef i)) (H i))))))) hds).