proposition: Lemma nth_beyond_idx : forall (l : list A) i, nth_error l i = None -> i >= length l.
proof: Proof. induction l; simpl; intro i. auto with arith. destruct i; simpl. intros. discr. intro. assert (i >= length l). apply (IHl i); trivial. auto with arith. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)