apply go_getRef_aux
α : 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
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig w input newWidth curr hcurr s).stream.getRef idx✝ ⋯ = (s.getRef idx✝ hidx✝).cast ⋯
no goals