Sequence filter respects Seq.append

SequenceFilterProperty.fst

module SequenceFilterProperty

open FStar.Seq 

let uint = UInt32.t

let pair = uint & uint
 
let rec snds_having_fst (i: uint) (e: seq pair)
  : Tot (seq uint)
        (decreases length e) =
 if length e = 0 then empty else  
   let f = fst (head e) in
     let s = snd (head e) in
       let sl' = snds_having_fst i (tail e) in
         if f = i 
         then cons s sl' 
         else sl' 


let rec snds_having_fst_respects_append (i: uint) 
                                        (l: seq pair)
                                        (r: seq pair)
                                        (s: seq pair{s == Seq.append l r})
  : Lemma (ensures snds_having_fst i s == Seq.append (snds_having_fst i l) (snds_having_fst i r)) 
          (decreases length l) =
  if length l = 0 then begin    
    lemma_eq_elim (append l r) r;
    lemma_eq_elim (snds_having_fst i l `append` snds_having_fst i r) (snds_having_fst i r)
  end else begin
    lemma_eq_elim (tail s) (tail l `append` r);
    snds_having_fst_respects_append i (tail l) r (tail s); 
    let h = head l in 
    if fst h = i then begin 
      lemma_eq_elim (cons (snd h) (snds_having_fst i (tail l) `append` snds_having_fst i r))       
                    (snds_having_fst i l `append` snds_having_fst i r)
    end else begin 
      lemma_eq_elim ((snds_having_fst i (tail l) `append` snds_having_fst i r)) 
                    (snds_having_fst i l `append` snds_having_fst i r)
    end 
  end