fact: Definition perm_dec (S : {set {set T}}) s : {set {perm T}} := [set restr_perm X s | X in S].
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp