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.