proposition: Lemma pvalues_eq : forall n (f g : forall i, i < n -> A), (forall i (hi : i < n), f i hi = g i hi) -> pvalues f = pvalues g.
proof: Proof. induction n; intros; simpl. refl. apply cons_eq. apply H. apply IHn. intros. apply H. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)