generalize hgo : go aig curr s hcurr lhs rhs f = res
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
⊢ ⟦{ aig := (go aig curr s hcurr lhs rhs f).aig, ref := (go aig curr s hcurr lhs rhs f).stream.getRef idx hidx1 },
      assign⟧ =
    ⟦f aig { lhs := lhs.getRef idx hidx1, rhs := rhs.getRef idx hidx1 }, assign⟧
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
hgo : go aig curr s hcurr lhs rhs f = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ =
    ⟦f aig { lhs := lhs.getRef idx hidx1, rhs := rhs.getRef idx hidx1 }, assign⟧