help on finite sequences

[Venkatesh Phadnavis <vphadnav@eecs.ku.edu>]

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
about how to go about this proof?

Thanks for your help,

Venkatesh.