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