proposition: Lemma pmap_lookup_insert_eq : forall (m : pmap) (k : positive) (v : T), pmap_lookup k (pmap_insert k v m) = Some v.
proof: Proof. intros m k; revert m. induction k; simpl; intros; forward; Cases.rewrite_all_goal; eauto. Qed.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases