fact: Fixpoint shrink (l :list A) : list A := match l with | nil => nil | x::l => if In_dec eq_dec x (shrink l) then cut eq_dec x (shrink l) else x::(shrink l) end.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)