Proving "each element in a sequence is 0 ==> the element at each index of the sequence is 0" is counterintuitive. How to reason about it?

lemma blah(p:nat->bool, xs:seq<nat>)
  requires forall t | t in xs :: p(t)
  ensures forall i | 0 <= i < |xs| :: p(xs[i]) {}

lemma zero_is_zero(xs:seq<nat>)
  requires forall x | x in xs :: (x == 0)
  ensures forall k | 0 <= k < |xs| :: (xs[k] == 0) {
  // blah(x => x == 0, xs);
}

So, I am trying out dafny version 4.4.0 and am struggling to understand the code-snippet above. It roughly matches one of the two relevant lemmas here; but I've simplified them a bit.

My understanding is that the zero_is_zero lemma is basically a generalization of the blah lemma (with the property p in this case being x => x == 0). So, if anything, it should be easier to automatically verify zero_is_zero. I was expecting that an element in the sequence would be considered indistinguishable from the same element when accessed through an index.

In practice, it turns out that blah is automatically verified (i.e. I don't have do do anything in the lemma body). But for zero_is_zero I have to explicitly invoke blah to show that it indeed holds for the property x => x == 0, and then suddenly it's not a problem anymore.

What is the explanation for this?

Thanks!

In Dafny the concept of triggers is important for any existential or forall operator. Here you have specified that x in xs as the trigger for a value to be zero. Therefore, you need to invoke that trigger to get the sequence to verify.

lemma zero_is_zero(xs:seq<nat>)
  requires forall x | x in xs :: (x == 0)
  ensures forall k | 0 <= k < |xs| :: (xs[k] == 0) 
{
    forall k | 0 <= k < |xs|
        ensures xs[k] == 0
    {
      assert xs[k] in xs;
    }
}