unfold go
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (go w hw input newWidth curr hcurr✝ s).getRef idx hidx1 =
    if hidx2 : idx < w then input.getRef idx ⋯ else input.getRef (w - 1) ⋯
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (if hcurr1 : curr < newWidth then
          if hcurr2 : curr < w then
            let s := s.pushRef (input.getRef curr hcurr2);
            go w hw input newWidth (curr + 1) ⋯ s
          else
            let s := s.pushRef (input.getRef (w - 1) ⋯);
            go w hw input newWidth (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).getRef
      idx hidx1 =
    if hidx2 : idx < w then input.getRef idx ⋯ else input.getRef (w - 1) ⋯