Prove theorem about seq(i,f)

Question

I would like to prove the following theorem

lemma seq_thm<T>(j:nat,f:nat ~> T)
requires forall i :: 0 <= i < j ==> f.requires(i)
ensures forall i :: 0 <= i < j ==> seq(j,f)[i] == f(i)

I expect this to be a fundamental theorem of the seq function, and would be invoked automatically by the SMT solver. However, it is not.

This lemma would be quite useful in a number of proof involving the seq function.

I tried to use a forall block to prove it, but it does not work.

{
  forall i | 0 <= i < j
  ensures seq(j,f)[i] == f(i)
  {
    assert seq(j,f)[i] == f(i);
  }
}

Answer 1

lemma seq_thm_k<T(==)>(j:nat,f:nat ~> T, k: nat, ss: seq<T>)
    requires j > 0
    requires forall i :: 0 <= i < j ==> f.requires(i)
    requires ss == seq(j, (i:nat) requires 0 <= i < j && f.requires(i) reads f.reads => f(i))
    requires k < j
    ensures ss[k] == f(k)
{
}

lemma seq_thm<T>(j:nat,f:nat ~> T)
requires forall i :: 0 <= i < j ==> f.requires(i)
ensures forall i :: 0 <= i < j ==> seq(j,(i:nat) requires 0 <= i < j && f.requires(i) reads f.reads => f(i))[i] == f(i)
{
}