Theorem: condFlipBit_apply_comm (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c d : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit i c) ((condFlipBit i d) q) = (condFlipBit i d) ((condFlipBit i c) q)
Tactic:
simp_rw [condFlipBit_apply_eq_mergeBitRes, getRes_mergeBitRes,
  getBit_mergeBitRes, Bool.xor_left_comm]
State after:
no goals