proposition: Lemma pvalues_ith_eq_map : forall l, pvalues (@f_ith l) = map f l.
proof: Proof. induction l; intros; unfold f_ith; simpl. refl. apply tail_eq. rewrite <- IHl. apply pvalues_eq. intros. unfold f_ith. f_equal. apply ith_eq. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)