Theorem: mergeBitRes_base_true (Controlbits/BitResiduum.lean)

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

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