∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} (aig : Std.Sat.AIG α) (idx : ℕ) (s : aig.RefVec idx)
  (hidx : idx ≤ len) (lhs rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α f],
  Std.Sat.AIG.RefVec.zip.go aig idx s hidx lhs rhs f =
    if hidx : idx < len then
      let res := f aig { lhs := lhs.get idx hidx, rhs := rhs.get idx hidx };
      let aig_1 := res.aig;
      have newRef := res.ref;
      have this := ⋯;
      have s := s.cast this;
      have s := s.push newRef;
      Std.Sat.AIG.RefVec.zip.go aig_1 (idx + 1) s ⋯ (lhs.cast this) (rhs.cast this) f
    else
      have this := ⋯;
      { aig := aig, vec := this ▸ s }