proposition: Theorem ptree_fold_correct : forall A (f : A -> T -> A) acc p, ptree_fold f p acc = fold_left f (ptree_to_list p) acc.
proof: Proof. intros A f acc p. revert acc. induction p as [v l IH] using ptree_ind'. simpl. intros acc. generalize (f acc v). clear acc. induction IH as [|q l H1 _ H2] ; simpl ; intros acc. easy. rewrite fold_left_app. rewrite H2. now apply f_equal. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)