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