proposition: Lemma nth_error_in_bounds: forall {A} (l: list A) i, (O <= i < length l)%nat -> exists x, nth_error l i = value x.
proof: Proof. intros until i; intros H. revert i l H. induction i; destruct l; intros; simpl in *; try solve [eauto | lia]. apply IHi; lia. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver