proposition: Lemma indices_complete : forall i x, x < i -> f x = a -> In x (indices i).
proof: Proof. intros i x xi e. apply indices_aux_complete; hyp. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)