Skip to content
Snippets Groups Projects
Commit ae1dd86c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Support `elements` in `set_solver`.

parent 3c484ebe
No related branches found
No related tags found
1 merge request!56Notion of (in)finite predicates
......@@ -35,6 +35,10 @@ Proof.
Defined.
(** * The [elements] operation *)
Global Instance set_unfold_elements X x P :
SetUnfold (x X) P SetUnfold (x elements X) P.
Proof. constructor. by rewrite elem_of_elements, (set_unfold (x X) P). Qed.
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Proof.
intros ?? E. apply NoDup_Permutation.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment