Broadcast proof with `where` clause needs explicit `where` to trigger

[jaylorch]

The following example doesn't verify unless you uncomment the where clause. It seems like this shouldn't be needed, since it's obvious that u32 implements PartialEq.

pub spec fn set_contains_element_opaque<T>(s: Set<T>, k: T) -> bool
    where
        T: PartialEq;

pub broadcast proof fn axiom_set_contains_element_opaque<T>(s: Set<T>, k: T)
    where
        T: PartialEq,
    ensures
        #[trigger] set_contains_element_opaque::<T>(s, k) <==> s.contains(k)
{
    admit();
}

fn test_axiom(s: Set<u32>, x: u32)
//    where u32: PartialEq,  // <== doesn't verify unless this clause is present
    requires
        set_contains_element_opaque(s, x)
    ensures
        s.contains(x)
{
    broadcast use axiom_set_contains_element_opaque;
}

[Chris-Hawblitzel]

Can you try it now?

[jaylorch]

Yep, it works now. Thanks!