proposition: Lemma elements_disj_union (X Y : C) : X ## Y → elements (X ∪ Y) ≡ₚ elements X ++ elements Y.
proof: Proof. intros HXY. apply NoDup_Permutation. - apply NoDup_elements. - apply NoDup_app. set_solver by eauto using NoDup_elements. - set_solver. Qed.
imports: stdpp(relations) stdpp(options)