proposition: Lemma nth_pos d : forall l, In x l -> nth (pos l) l d = x.
proof: Proof. induction l; intro h; simpl. fo. destruct (eq_dec a x). hyp. apply IHl. fo. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)