simp [bitwise_getBit]
case a
l m n i : Nat
⊢ getBit (bitwise and (bitwise bne l m) n) i = getBit (bitwise bne (bitwise and l n) (bitwise and m n)) i
case a
l m n i : Nat
⊢ (getBit l i != getBit m i && getBit n i) = ((getBit l i && getBit n i) != (getBit m i && getBit n i))