Surprising incompleteness in a proof about Seq::filter

[ahuoguo]

In the following code, I need to assert the postcondition of the lemma call to verify, which is quite unexpected.

use vstd::prelude::*;

verus! {

pub proof fn seq_filter_is_a_subset_of_original_seq<A>(s: Seq<A>, pred: spec_fn(A) -> bool)
    ensures
        forall |i: int| #![all_triggers] 0 <= i < s.filter(pred).len() ==> s.contains(s.filter(pred)[i])
    decreases s.len()
{
    assert forall |i: int| 0 <= i < s.filter(pred).len() implies s.contains(#[trigger] s.filter(pred)[i]) by {
        reveal(Seq::filter);
        let subseq = s.drop_last();
        seq_filter_is_a_subset_of_original_seq(subseq, pred);

        // TODO: why the following assert have to be repeated even tho
        // it's exactly the same as the postcondition of the lemma call above
        // assert(forall |i: int| 0 <= i < subseq.filter(pred).len() ==> subseq.contains(#[trigger] subseq.filter(pred)[i]));
    }
}
}

fn main() {}

verus playground link

The air code has similar behavior. I need to assert the body of (ens%hi!seq_filter_is_a_subset_of_original_seq. A&. A& subseq@ pred!) to make it verify.

wo-assert.air.zip