proposition: Lemma elements_list_to_set l : NoDup l → elements (list_to_set (C:=C) l) ≡ₚ l.
proof: Proof. intros Hl. induction Hl. { rewrite list_to_set_nil. rewrite elements_empty. done. } rewrite list_to_set_cons, elements_disj_union by set_solver. rewrite elements_singleton. apply Permutation_skip. done. Qed.
imports: stdpp(relations) stdpp(options)