Theorem: condFlipBit_zero_mergeBitRes_false (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
c : BV a✝ → Bool
p : BV a✝
⊢ (condFlipBit 0 c) (mergeBitRes 0 false p) = finProdFinEquiv (p, bif c p then 1 else 0)
Tactic:
simp_rw [condFlipBit_zero_mergeBitRes, Bool.xor_false]
State after:
no goals