proposition: Lemma indices_aux_length : forall i acc, length (indices_aux acc i) <= i + length acc.
proof: Proof. induction i; simpl; intros. refl. destruct (eq_dec (f i) a). ded (IHi (i::acc)). simpl in H. lia. ded (IHi acc). lia. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)