proposition: Lemma pmap_lookup_insert_neq : forall (m : pmap) (k : positive) (v : T) (k' : positive), k <> k' -> forall v' : T, pmap_lookup k' (pmap_insert k v m) = pmap_lookup k' m.
proof: Proof. intros. remember (pmap_lookup k' m). destruct o; [ apply pmap_lookup_insert_Some_neq; intuition | apply pmap_lookup_insert_None_neq; intuition]. Qed.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases