fact: Fixpoint pmap_elim (R : Type) (ts : pmap T) : Type := match ts with | Empty => R | Branch None l r => pmap_elim (pmap_elim R r) l | Branch (Some x) l r => F x -> pmap_elim (pmap_elim R r) l end.
imports: Coq(PArith) ExtLib.Data.Map.FMapPositive ExtLib.Data.Eq ExtLib.Tactics.Injection Coq(PArith)