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