proposition: Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
proof: Proof. apply Permutation_singleton_r. by rewrite <-(right_id ∅ (∪) {[x]}), elements_union_singleton, elements_empty by set_solver. Qed.
imports: stdpp(relations) stdpp(options)