proposition: Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X.
proof: Proof. revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|]. rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|]. apply IH in Hin; set_solver. Qed.
imports: stdpp(relations) stdpp(options)