fact: Definition fiber (P : set) B (f : elts P -> B) b : set := fun x => exists h : mem x P, f (elt h) = b.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)