fact: Fixpoint mem' {A: Type} (i: key) (t: ptrie A) := match t with | Empty => false | Leaf k v => eqb i k | Branch prefix brbit l r => if zerobit i brbit then mem' i l else mem' i r end.
imports: List Bool ZArith Lia