proposition: Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
proof: Proof. unfold size, set_size. simpl. rewrite <-!elem_of_elements. generalize (elements X). intros [|? l]; intro; simplify_eq/=. rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence. Qed.
imports: stdpp(relations) stdpp(options)