proposition: Lemma In_indices_aux_elim : forall i x acc, In x (indices_aux acc i) -> In x acc \/ (f x = a /\ x < i).
proof: Proof. induction i; simpl; intros. auto. destruct (eq_dec (f i) a); destruct (IHi _ _ H); intuition. destruct H0. subst. auto. auto. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)