∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ}
  (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [inst_3 : Std.Sat.AIG.RefVec.LawfulMapOperator α f]
  (_x : (aig : Std.Sat.AIG α) ×' (i : ℕ) ×' (_ : i ≤ len) ×' (_ : aig.RefVec i) ×' aig.RefVec len) (idx : ℕ)
  (h1 : idx < _x.1.decls.size)
  (h2 : idx < (Std.Sat.AIG.RefVec.map.go _x.1 _x.2.1 ⋯ _x.2.2.2.1 _x.2.2.2.2 f).aig.decls.size),
  (Std.Sat.AIG.RefVec.map.go _x.1 _x.2.1 ⋯ _x.2.2.2.1 _x.2.2.2.2 f).aig.decls[idx] = _x.1.decls[idx]