fact: Fixpoint update {A: Type} (f : A -> option A ) (i: key) (m: ptrie A) : ptrie A := match m with | Empty => Empty | Leaf j v => if eqb i j then match f v with | None => Empty | Some v' => Leaf i v' end else Leaf j v | Branch prefix brbit l r => if match_prefix i prefix brbit then if zerobit i brbit then branch prefix brbit (update f i l) r else branch prefix brbit l (update f i r) else m end.
imports: List Bool ZArith Lia