∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (decls : Array (Std.Sat.AIG.Decl α))
  (cache : Std.Sat.AIG.Cache α decls) (decl : Std.Sat.AIG.Decl α),
  Std.Sat.AIG.Cache.WF (decls.push decl) ((↑cache).insert decl decls.size)