fact: Record fibered_set := FiberedSet { carrier : finType; elt : carrier; fbset :> {set carrier}; fbfun : carrier -> I }.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype finset)