Solving goals for set operations
set_solver
seems quite fast for solving simple goals with set operations, but fails on the goal below. Is there a more powerful (maybe slower) tactic that can solve this?
Require Import stdpp.set.
Goal
forall A (s1 s2: set A) (x: A),
set_intersection s1 s2 = set_empty ->
set_elem_of x s1 ->
set_elem_of x s2 ->
False.
set_solver.