proposition: Lemma In_indices_aux_intro : forall i x acc, In x acc -> In x (indices_aux acc i).
proof: Proof. induction i; simpl; intros. hyp. destruct (eq_dec (f i) a). apply IHi. simpl. auto. apply IHi. hyp. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)