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