proposition: Lemma afa_ex3_inv a : a = singleton (\Po (\Po a)) -> exists b c d, [/\ a = singleton b, b = (doubleton emptyset (singleton emptyset)) +s1 c +s1 d, c = doubleton emptyset a & d = singleton a].
proof: Proof. set b := (\Po (\Po a)) => av; exists b. move: (setP_1 b); rewrite - av; set c := doubleton emptyset a => h. set d:= singleton a;exists c, d; split => //. set_extens t. move => /setP_P; rewrite av; rewrite setP_1 - av => ct. case: (inc_or_not emptyset t);case: (inc_or_not a t) => ha hb. - apply: setU1_r; apply/setU1_P; right; set_extens u; first by move/ct. by case/set2_P => ->. - apply: setU1_r;apply: setU1_r; apply/set2_P; right. by apply:(set1_pr hb) => u ut; case/set2_P:(ct _ ut) => // ua; case: ha;ue. - apply/setU1_P; right; apply:(set1_pr ha) => u ut. case/set2_P:(ct _ ut) => // ua; case: hb;ue. - apply: setU1_r;apply: setU1_r; apply/set2_P; left; apply/set0_P => u ut. case/set2_P:(ct _ ut) => hc; [ case: hb; ue | case: ha;ue]. case/setU1_P; last by move ->; apply /setP_P => u /set1_P ->; apply: setP_Ti. case/setU1_P; last by move ->; rewrite - h; apply: setP_Ti. case /set2_P => ->; first by apply: setP_0i. by apply /setP_P => u /set1_P ->; apply:setP_0i. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)