proposition: Lemma NoDup_fresh_list n X : NoDup (fresh_list n X).
proof: Proof. revert X. induction n; simpl; constructor; auto. intros Hin; apply fresh_list_is_fresh in Hin; set_solver. Qed.
imports: stdpp(relations) stdpp(options)