proposition: Lemma afa_ex3 a b c d: a = singleton b -> b = (doubleton emptyset (singleton emptyset)) +s1 c +s1 d -> c = doubleton emptyset a -> d = singleton a -> a = singleton (\Po (\Po a)).
proof: Proof. move => av bv cv dv; rewrite av setP_1 {1} bv -av; congr (singleton _). set_extens t. move => h; apply/setP_P; case /setU1_P :h. case /setU1_P. case /set2_P => ->; fprops;apply : set1_sub; fprops. move => ->; rewrite - cv; fprops. move => ->; rewrite dv; apply : set1_sub; fprops. move /setP_P => h. case: (inc_or_not emptyset t) => ta; case: (inc_or_not a t) => tb. - apply /setU1_P; left; apply /setU1_P; right; rewrite cv. by apply: extensionality => // => s; case /set2_P => ->. - apply /setU1_P; left; apply /setU1_P; left; apply /set2_P; right. apply set1_pr => // s st; move: (h _ st); case /set2_P => // sa; case: tb; ue. - apply /setU1_P; right; rewrite dv; apply set1_pr => // s st. move: (h _ st); case /set2_P => // sa; case: ta; ue. - apply /setU1_P; left; apply /setU1_P; left; apply /set2_P; left. apply /set0_P => // s st; move: (h _ st); case /set2_P => sa. case: ta; ue. case: tb; ue. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)