fact: Fixpoint set' (A: Type) (i: elt) (x: A) (t: ptrie A) := match t with | Empty => Leaf i x | Leaf j v => if elt_eqb i j then Leaf i x else join i (Leaf i x) j (Leaf j v) | Branch prefix brbit l r => if Key.match_prefix i prefix brbit then if Key.zerobit i brbit then Branch prefix brbit (set' i x l) r else Branch prefix brbit l (set' i x r) else join i (Leaf i x) prefix (Branch prefix brbit l r) end.
imports: Lia Cdcl.Coqlib