Theorem: getBit_mergeBitRes (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
b : Bool
p : BV a✝
⊢ getBit i (mergeBitRes i b p) = b
Tactic:
simp_rw [getBit_apply, mergeBitRes_apply, Equiv.apply_symm_apply]
State after:
no goals