Install/export module with inspect definition and notation like eqn

[palmskog]

The inspect pattern relies on the following definition and notation:

Definition inspect {A} (a : A) : {b | a = b} :=
  exist _ a eq_refl.

Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).

While inspect is available in the module Prop.Logic, it is not imported by From Equations Require Import Equations, and there is no installed module with the eqn notation or anything like it installed by the coq-equations package. This means that practically everyone who wants to use the inspect pattern effectively has to bundle (copy paste) a version of this definition and notation in their project.

A better solution would be to provide this definition and notation in some installed module that is exported by default. Reasonably, the notation should be inside a scope to avoid clashes with similar notations. For example, eqn clashes with destruct x eqn:H.