proposition: Lemma pmap_lookup_insert_empty : forall k k' v, k <> k' -> pmap_lookup k' (pmap_insert k v Empty) = None.
proof: Proof. induction k; destruct k'; simpl; intros; eauto using tilde_0_inj_neg, tilde_1_inj_neg. destruct k'; simpl; auto. destruct k'; simpl; auto. destruct k'; simpl; auto. destruct k'; simpl; auto. congruence. Qed.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases