Theorem: condFlipBit_zero_mergeBitRes_true (Controlbits/BitResiduum.lean)

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