fact: Fixpoint pmap_lookup'_Empty (p : positive) : pmap_lookup' Empty p = None := match p with | xH => eq_refl | xO p => pmap_lookup'_Empty p | xI p => pmap_lookup'_Empty p end.
imports: Coq(PArith) ExtLib.Data.Map.FMapPositive ExtLib.Data.Eq ExtLib.Tactics.Injection Coq(PArith)