Function lemma_usize_setbit_bit_is_set 

pub broadcast proof fn lemma_usize_setbit_bit_is_set(word: usize, b: int)

requires

0 <= b < usize::BITS as int,

ensures

usize_bit_is_set(word | (1usize << (b as usize)), b),

Setting bit b makes that bit set.