proposition: Lemma exercise1_4 X x: sub X (singleton x) <-> (X = singleton x \/ X = emptyset).
proof: Proof. split; last by case => ->; fprops. move => asx; case: (emptyset_dichot X); first by right. by move => nea; left; apply: set1_pr1 => // z /asx /set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)