Broadcast not in scope during loop

[jaylorch]

The following code fails verification because the broadcast use is somehow not in scope during the loop.

pub spec fn map_contains_key_opaque<Key, Value>(m: Map<Key, Value>, k: Key) -> bool;

pub broadcast proof fn axiom_map_contains_key_opaque<Key, Value>(m: Map<Key, Value>, k: Key)
    ensures
        #[trigger] map_contains_key_opaque::<Key, Value>(m, k) <==> m.contains_key(k)
{
    admit();
}

fn test_axiom(m: Map<u64, u32>, k: u64)
    requires
        map_contains_key_opaque(m, k)
{
    broadcast use axiom_map_contains_key_opaque;
    for i in 0..10
        invariant
            map_contains_key_opaque(m, k)
    {
        assert(m.contains_key(k)) by {
//            broadcast use axiom_map_contains_key_opaque; // <== needs this to verify
        }
    }
}

[utaal]

@Chris-Hawblitzel I can also take a look at this if you'd like.