fact: Fixpoint indices_aux acc i := match i with | 0 => acc | S i' => indices_aux (if eq_dec (f i') a then i' :: acc else acc) i' end.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)