Function lemma_u128_setbit_bit_is_set 

pub broadcast proof fn lemma_u128_setbit_bit_is_set(word: u128, b: int)

requires

0 <= b < 128,

ensures

u128_bit_is_set(word | (1u128 << (b as usize)), b),

Setting bit b makes that bit set.