proposition: Lemma powerset_injective: injective powerset.
proof: Proof. move => x y eq1; apply:extensionality. by move:(setP_Ti x); rewrite eq1 => /setP_P. by move:(setP_Ti y); rewrite - eq1 => /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)