I’m unable to prove the following basic property of a sequence comprehension.

  lemma LemmaSeqComprehension<T>(n: nat, fn: nat --> T, index: nat)
    requires forall i: nat :: i < n ==> fn.requires(i)
    requires index < n
    ensures seq(n, fn)[index] == fn(index)
  {
  }

What am I missing?