Function lemma_u64_setbit_bit_unchanged 

pub broadcast proof fn lemma_u64_setbit_bit_unchanged(word: u64, b: int, b2: int)

requires

0 <= b < 64,

0 <= b2 < 64,

b != b2,

ensures

u64_bit_is_set(word | (1u64 << (b as usize)), b2) == u64_bit_is_set(word, b2),

Setting bit b leaves a different in-range bit b2 unchanged.