∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  (c : Std.Sat.AIG.Cache α decls) (decl : Std.Sat.AIG.Decl α), (↑c)[decl]? = some idx → idx < decls.size