proposition: Lemma pmap_lookup_remove_eq : forall (m : pmap) (k : positive) (v : T), pmap_lookup k (pmap_remove k m) <> Some v.
proof: Proof. induction m; destruct k; simpl; intros; try congruence. { destruct o; simpl; eauto. destruct m1; simpl; eauto. destruct (pmap_remove k m2) eqn:?; try congruence. rewrite <- Heqp. eauto. } { destruct o; simpl; eauto. destruct (pmap_remove k m1) eqn:?; try congruence. - destruct m2; try congruence; eauto. destruct k; simpl; congruence. - rewrite <- Heqp. eauto. } { destruct m1; try congruence. destruct m2; try congruence. } Qed.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases