simp [Nat.lor_getBit, Nat.land_getBit]
case a
l m n i : Nat
⊢ getBit ((l ||| m) &&& n) i = getBit (l &&& n ||| 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)