fact: Fixpoint fold' {A B: Type} (f: B -> key -> A -> B) (m: ptrie A) (acc: B): B := match m with | Empty => acc | Leaf k v => f acc k v | Branch p m l r => fold' f r (fold' f l acc) end.
imports: List Bool ZArith Lia