simp [heq]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
assign : α → Bool
idx : Nat
hidx1 : idx < newWidth
hidx2 : curr ≤ idx
res : RefStreamEntry α newWidth
h✝ : curr < newWidth
heq : curr = idx
hsplit✝ : curr < w
hsplit : idx < w
hgo : go aig w input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr hsplit✝)) = res
⊢ ⟦{ aig := aig, ref := { gate := ((input.getRef curr hsplit✝).cast ⋯).gate, hgate := ?hstart } }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef idx ⋯ }, assign⟧
no goals