Function lemma_seq_to_set_map_contains Copy item path

pub broadcast proof fn lemma_seq_to_set_map_contains<T, U>(
    s: Seq<T>,
    f: FnSpec<(T,), U>,
    i: int,
)

0 <= i < s.len(),

(s.map_values(f)).to_set().contains(f(s[i])),