Tests for `set_unfold in H`.

f70ecc5c · Robbert Krebbers · bd0e6352 · f70ecc5c · f70ecc5c
Commit f70ecc5c authored 5 years ago by Robbert Krebbers
--- a/tests/sets.ref
+++ b/tests/sets.ref
--- a/tests/sets.v
+++ b/tests/sets.v
+From stdpp Require Import sets.
+Lemma foo `{Set_ A C} (x : A) (X Y : C) : x ∈ X ∩ Y → x ∈ X.
+Proof. intros Hx. set_unfold in Hx. tauto. Qed.