Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. 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.
(** To assume the Funext axiom outright, import this file.
    (Doing this instead of simply positing Funext directly
    avoids creating multiple witnesses for the axiom in
    different developments.) *)

[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Axiom funext_axiom : Funext. Global Existing Instance funext_axiom.