Theorem: getBitRes_succAbove_symm_apply (Controlbits/BitResiduum.lean)

State before:
m : ℕ
b : Bool
p : BV (m + 1)
j : Fin (m + 2)
i : Fin (m + 1)
⊢ (getBitRes (j.succAbove i)).symm (b, p) =
    (getBitRes j).symm (((getBitRes (i.predAbove j)) p).1, (getBitRes i).symm (b, ((getBitRes (i.predAbove j)) p).2))
Tactic:
rw [getBitRes_succAbove, getBitResSuccAbove_symm_apply]
State after:
no goals