proposition: Lemma afa_ex2_inv a: a = singleton (\Po a) -> exists b, a = singleton b /\ b = doubleton emptyset a.
proof: Proof. set b := \Po a => eq1; exists b; split => //. by move: (setP_1 b); rewrite - eq1. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)