 # How can I use destruct given the constraint I have for index range of a list?

Hi,

I’m trying to prove that for a list of bytes `a`, all bytes are `x01` from index `2` to `(n-m-2)`, where `n` is the length of `a`:

`(forall (i : nat), ((i >= 2) /\ (i < ((n - m) - 1))) -> ((nth_error a i) = (Some x01)))`

And in the context I do have this:

``````H : nth_error a ?j =
nth_error ([x00; x00] ++ repeat x01 (n - m - 2) ++ repeat x00 m)%list  ?j
``````

So, after `intros i i_range.` I have:

``````i : nat
i_range : is_true (1 < i) /\ is_true (i < n - m - 1)
H : nth_error a ?j =
nth_error ([x00; x00] ++ repeat x01 (n - m - 2) ++ repeat x00 m)%list  ?j
______________________________________(1/1)
nth_error a i = Some x01
``````

Is this a right approach to destruct RHS of `H` to eliminate the first two bytes and the last `m` bytes? If so, how can I do that with respect to `i_range`? Let me know if my proof strategy is flawed.

Thanks in advance for any suggestion.

This question has been answered here: