-
Paolo G. Giarrusso authored
`set_unfold_bind` for sets already exists; this brings the list variant on par.
Paolo G. Giarrusso authored`set_unfold_bind` for sets already exists; this brings the list variant on par.
sets.v 323 B
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.
(** Test [set_unfold_list_bind]. *)
Lemma elem_of_list_bind_again {A B} (x : B) (l : list A) f :
x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
Proof. set_solver. Qed.