fact: Fixpoint ptree_fold {A} (f : A -> T -> A) (p : ptree) (acc : A) : A := match p with | PTsome v l => fold_left (fun acc q => ptree_fold f q acc) l (f acc v) end.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)