proposition: Lemma list_to_set_inj n: injective (fun s: n.-tuple bool => list_to_set n s).
proof: Proof. move => a b /= fab; apply:val_inj. rewrite /= -(list_to_setK (size_tuple a)). by rewrite -(list_to_setK (size_tuple b)) fab. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)