proposition: Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
proof: Proof. destruct X as [l]; split; [|by intros; simplify_eq/=]. rewrite elem_of_equiv_empty; intros Hl. destruct l as [|x l]; [done|]. oinversion Hl. left. Qed.
imports: stdpp(options)