Theorem: mergeBitRes_base_false (Controlbits/BitResiduum.lean)

State before:
i : Fin (0 + 1)
p : BV 0
⊢ mergeBitRes i false p = 0
Tactic:
rw [Fin.eq_zero p]
State after:
i : Fin (0 + 1)
p : BV 0
⊢ mergeBitRes i false 0 = 0

State before:
i : Fin (0 + 1)
p : BV 0
⊢ mergeBitRes i false 0 = 0
Tactic:
exact mergeBitRes_apply_false_zero
State after:
no goals