Theorem: condFlipBit_apply_comm_flipBit (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit i c) ((flipBit i) q) = (flipBit i) ((condFlipBit i c) q)
Tactic:
rw [condFlipBit_flipBit_of_all_true, condFlipBit_apply_comm]
State after:
no goals