unfold go at hgo
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo : go aig curr hcurr cin s lhs rhs = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      let lin := lhs.getRef curr hidx;
      let rin := rhs.getRef curr hidx;
      let res := mkFullAdder aig { lhs := lin, rhs := rin, cin := cin };
      let aig_1 := res.aig;
      let outRef := res.out;
      let carryRef := res.cout;
      let s := s.cast ⋯;
      let lhs := lhs.cast ⋯;
      let rhs := rhs.cast ⋯;
      let s := s.pushRef outRef;
      go aig_1 (curr + 1) ⋯ carryRef s lhs rhs
    else
      let_fun hcurr := ⋯;
      { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]