Theorem: condFlipBit_zero_mergeBitRes (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
c : BV a✝ → Bool
b : Bool
p : BV a✝
⊢ (condFlipBit 0 c) (mergeBitRes 0 b p) = finProdFinEquiv (p, bif xor (c p) b then 1 else 0)
Tactic:
simp_rw [condFlipBit_mergeBitRes, mergeBitRes_zero]
State after:
no goals