unfold go at hgo
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
hgo : go aig curr hcurr cin 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 α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
hgo :
  (if hidx : curr < a✝ then
      let lin := lhs.getRef curr hidx;
      let rin := rhs.getRef curr hidx;
      let res := mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
      let_fun this := ⋯;
      let aig_1 := res.aig;
      let carryRef := res.ref;
      let lhs_1 := lhs.cast this;
      let rhs_1 := rhs.cast this;
      go aig_1 (curr + 1) ⋯ carryRef lhs_1 rhs_1
    else { aig := aig, ref := cin }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]