missed case in recursive type-checking

[tjhance]

This ought to fail the type well-founded-recursion-checking, but it doesn't:

struct Qux<T> {
    t: T,
}

struct Bar<T> {
    s: Box<Set<Qux<T>>>,
}

struct Foo {
    bar: Bar<Foo>,
}

e.g. you can do the usual russell's paradox set-of-sets-that-do-not-contain themselves:

proof fn prove_false()
    ensures false
{
    let s = Set::<Qux<Foo>>::new(
        |qux: Qux<Foo>| !qux.t.bar.s.contains(qux)
    );
    let qux = Qux{ t: Foo { bar: Bar { s: box s } } };
    assert(qux.t.bar.s.contains(qux));
    assert(!qux.t.bar.s.contains(qux));
    assert(false);
}