cases l.getBit i <;> cases m.getBit i <;> cases n.getBit i <;> decide
case a
l m n i : Nat
⊢ (getBit l i && getBit m i != getBit n i) = ((getBit l i && getBit m i) != (getBit l i && getBit n i))
no goals