Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file extraction_plugin.cmxs (using legacy method) ... done]
[Loading ML file equations_plugin.cmxs (using legacy method) ... done]

Export Equations.Prop.Logic.

Utility: Equations Definitions

The inspect definition is used to pack a value with a proof of an equality to itself. When pattern matching on the first component in this existential type, we keep information about the origin of the pattern available in the second component, the equality.
See 
Notation "x 'eq:' p" := (exist _ x p) (only parsing, at level 20).

(* required for documentation generation *)
Definition iYC2 := True.