proposition: Lemma list_In_nth : forall (l : list A) a, In a l -> exists p: nat, nth_error l p = Some a.
proof: Proof. induction l. contr. intros; destruct H. exists 0. rewrite H; trivial. destruct (IHl a0 H). exists (S x); trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)