proposition: Lemma nth_some_in : forall (l : list A) i a, nth_error l i = Some a -> In a l.
proof: Proof. induction l; intros. destruct i; simpl in *; discr. destruct i; simpl in *. left; compute in *; congruence. right; eapply IHl; eauto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)