proposition: Lemma nth_error_In : forall (l : list A) i, {a : A | nth_error l i = Some a} + {nth_error l i = None}.
proof: Proof. induction l. right; compute; case i; trivial. intro i. case i. left; exists a; trivial. intro n. destruct (IHl n) as [[a' a'nth] | nth_none]. left; exists a'; trivial. right; trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)