Theorem: getBit_condFlipBit' (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ getBit i ((condFlipBit i c) q) = xor (c (getRes i q)) (getBit i q)
Tactic:
rcases (c (getRes i q)).dichotomy with hc | hc <;>
simp only [condFlipBit_apply, hc, cond_false, cond_true,
  Bool.false_xor, Bool.true_xor, getBit_flipBit]
State after:
no goals