proposition: Lemma indices_correct : forall i x, In x (indices i) -> f x = a /\ x < i.
proof: Proof. intros i x h. destruct (In_indices_aux_elim h). inversion H. hyp. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)