fact: Definition branch (o : option T) (l r : pmap) : pmap := match o , l , r with | None , Empty , Empty => Empty | _ , _ , _ => Branch o l r end.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases