proposition: Lemma lookup_empty : forall k, pmap_lookup k Empty = None.
proof: Proof. destruct k; reflexivity. Qed.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases