fact: Definition join (A: Type) (k1: Key.t) (t1: ptrie A) (k2: Key.t) (t2: ptrie A) := let m := Key.branching_bit k1 k2 in if Key.zerobit k1 m then Branch (Key.mask k1 m) m t1 t2 else Branch (Key.mask k1 m) m t2 t1.
imports: Lia Cdcl.Coqlib