proposition: Lemma prefix_correct : (forall i, f (i0 + g i) = a) -> (forall i, f (prefix i) = a).
proof: Proof. intros hg i. unfold prefix. destruct (lt_dec i (length (indices i0))). eapply indices_correct. apply nth_In. hyp. apply hg. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)