proposition: Lemma CForall_indexed {A} (P: A -> Type) (l: list A): CForall P l -> forall i (d: A), (i < length l)%nat -> P (nth i l d).
proof: Proof. intros X i. revert l X. induction i; destruct l; simpl in *; intuition; exfalso; inversion H. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)