proposition: Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
proof: Proof. intros E. destruct (size_pos_elem_of X) as [x ?]; auto with lia. exists x. apply set_equiv. split. - rewrite elem_of_singleton. eauto using size_singleton_inv. - set_solver. Qed.
imports: stdpp(relations) stdpp(options)