proposition: Lemma pmap_lookup'_eq p m : pmap_lookup p m = pmap_lookup' m p.
proof: Proof. generalize dependent m. induction p; intuition. simpl. destruct m. simpl. rewrite pmap_lookup'_Empty. reflexivity. simpl in *. apply IHp. simpl in *. destruct m. simpl. rewrite pmap_lookup'_Empty. reflexivity. simpl. apply IHp. Defined.
imports: Coq(PArith) ExtLib.Data.Map.FMapPositive ExtLib.Data.Eq ExtLib.Tactics.Injection Coq(PArith)