Theorem: flipBit_flipBit (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ (flipBit i) ((flipBit i) q) = q
Tactic:
simp_rw [flipBit_apply (q := q), flipBit_mergeBitRes,
  Bool.not_not, mergeBitRes_getBit_getRes]
State after:
no goals