fact: Fixpoint pmap_lookup (p : positive) (m : pmap) {struct p} : option T := match m with | Empty => None | Branch d l r => match p with | xH => d | xO p => pmap_lookup p l | xI p => pmap_lookup p r end end.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases