help on finite sequences

```
Hello,

I am trying to prove a property about a finite_sequence that I build
recursively:

filter(fs: finite_sequence[T], k: below[fs`length], p: pred[T]):
RECURSIVE finite_sequence =
IF k = fs`length - 1 THEN
IF p(fs`seq(k)) THEN
(# length := 1,
seq := LAMBDA(n: below[1]): fs`seq(k) #)
ELSE
empty_seq[T]
ENDIF
ELSE
IF p(fs`seq(k)) THEN
o((# length := 1,
seq := LAMBDA(n: below[1]): fs`seq(k) #),
filter(fs, k+1, p)
ELSE
filter(fs, k+1, p)
ENDIF
ENDIF
MEASURE fs`length - k;

every_filter: LEMMA
FORALL (fs: finite_sequence[T], p: pred[T]):
LET filtered_sequence = filter(fs, 0, p) IN
FORALL (i: below[filtered_sequence`length]):
p(filtered_sequence`seq(i));

Essentially I am trying to say that every element of the sequence that is
built using filter(...) with predicate p satisfies the predicate p. This
looks really easy to prove except that I am unable to extract the ith
element of the filter(...) sequence, or the seq function that is being
built up. Ignoring the TCCS for the moment, does anyone have any ideas