proposition: Theorem card_setP X: cardinal (\Po X) = \2c ^c X.
proof: Proof. set K:= functions X \2c. apply/card_eqP; exists (Lf (char_fun ^~ X) (\Po X) K); hnf;saw. apply:lf_bijective. - move => y /setP_P yX; apply /functionsP;split => //; rewrite /char_fun; aww. by apply:char_fun_f. - by move => u v /setP_P uX /setP_P vX /(char_fun_injectiveP uX vX). - move => y /functionsP /char_fun_surjective [A /setP_P pa pb]; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)