T (match b with [true \Rightarrow (TLRef i) | false \Rightarrow (match b with
[true \Rightarrow (TLRef (pred i)) | false \Rightarrow (lift i O v)])]) (lift
i O v))) (refl_equal T (lift i O v)) (blt i i) (le_bge i i (le_n i)))).
T (match b with [true \Rightarrow (TLRef i) | false \Rightarrow (match b with
[true \Rightarrow (TLRef (pred i)) | false \Rightarrow (lift i O v)])]) (lift
i O v))) (refl_equal T (lift i O v)) (blt i i) (le_bge i i (le_n i)))).