proposition: Lemma powerset0 : powerset set0 = [set set0] :> {set {set T}}.
proof: Proof. by apply/setP=> A; rewrite set1.unlock !inE subset0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)