proposition: Lemma In_nth : forall A d (x : A) l, In x l -> exists i, i < length l /\ nth i l d = x.
proof: Proof. induction l; simpl; intros. contr. destruct H. subst. exists 0. intuition. destruct (IHl H) as [i hi]. exists (S i). intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)