fact: Fixpoint pmap_insert (p : positive) (v : T) (m : pmap) {struct p} : pmap := match p with | xH => Branch (Some v) (pmap_left m) (pmap_right m) | xO p => Branch (pmap_here m) (pmap_insert p v (pmap_left m)) (pmap_right m) | xI p => Branch (pmap_here m) (pmap_left m) (pmap_insert p v (pmap_right m)) end.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases