Example in the guide can't be verified.

[HaoYang670]

I am following the https://verus-lang.github.io/verus/guide/develop_proofs.html, but find

{
    if s1.is_empty() {
        assume(s1.intersect(s2).len() <= 0);
        assert(s1.intersect(s2).len() <= s1.len());
    } else {
        ...
    }
}

can't be verified.

[HaoYang670]

I don't know what happened. But when I tried it again today, it could work.