proposition: Lemma len_aux_ext : forall x (f g : forall y, R x y -> nat), (forall y (p : R x y), f y p = g y p) -> len_aux f = len_aux g.
proof: Proof. intros. unfold len_aux. apply (f_equal (fun l => S (lmax l))). apply pvalues_eq. intros. apply H. Qed.
imports: CoLoR(SN ListMax RelUtil ListUtil LogicUtil) Coq(Arith)