split <;> rfl
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{ aig := aig, ref := if h : idx✝ < rw✝ then rw.getRef idx✝ h else lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧ =
    if hr : idx✝ < rw✝ then ⟦{ aig := aig, ref := rw.getRef idx✝ hr }, assign⟧
    else ⟦{ aig := aig, ref := lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧
no goals