set_solver fails to prove simple goal
Hello,
I got stuck on the following example. Am I doing something wrong?
Require Import stdpp.set.
Goal forall {T} (x: T),
set_elem_of x (set_union set_empty (set_singleton x)).
set_solver.
Hello,
I got stuck on the following example. Am I doing something wrong?
Require Import stdpp.set.
Goal forall {T} (x: T),
set_elem_of x (set_union set_empty (set_singleton x)).
set_solver.