diff --git a/.gitignore b/.gitignore
index 67b16555a..cae3ca340 100644
--- a/.gitignore
+++ b/.gitignore
@@ -69,6 +69,9 @@ tests/fstar/misc/obj/
 *.uo
 *Theory.sml
 
+# Lean
+.lake
+
 # Misc
 /fstar-tests
 *~
diff --git a/docs/user/README.md b/docs/user/README.md
new file mode 100644
index 000000000..798fec305
--- /dev/null
+++ b/docs/user/README.md
@@ -0,0 +1,116 @@
+# Aeneas user documentation - developer docs
+
+## Architecture
+
+This is a separate `flake.nix` setup from the root repository's one, but it relies on Aeneas' Lean library from this repository.
+
+We pull Lean 4's upstream flake to build Lean in Nix, use some forked Alectryon-related tooling to assemble a mdBook HTML output.
+
+### How to add new files?
+
+If these files are not supposed to be inked by Alectryon (i.e. display interactive goals in the browser), they can be extended following [the vanilla mdBook documentation](https://rust-lang.github.io/mdBook/guide/creating.html) in the `src/` directory.
+
+If these files are supposed to be inked by Alectryon:
+
+- they need to appear in `src/lean/basics` as `xyz.lean` and `xyz.lean.md`
+- the Markdown file version should be included in the `SUMMARY.md` file.
+- the contents of `xyz.lean.md` by default should be the same as the others one, i.e. a Lean code block containing `{{#include xyz.lean}}`
+
+### How to add a new directory containing Lean files?
+
+This requires a change in the `flake.nix`, find the place where the `literate` package is defined:
+
+```nix
+      literate = buildLeanPackage {
+        name = "literate";
+        deps = [ aeneas-base ];
+        src = ./.;
+        roots = [
+          {
+            mod = "src/lean/basics";
+            glob = "submodules";
+          }
+        ];
+      };
+```
+
+Add a new `root` as it follows, assuming your new module is `src/lean/advanced`:
+
+```nix
+      literate = buildLeanPackage {
+        name = "literate";
+        deps = [ aeneas-base ];
+        src = ./.;
+        roots = [
+          {
+            mod = "src/lean/basics";
+            glob = "submodules";
+          }
+          {
+            mod = "src/lean/advanced";
+            glob = "submodules";
+         }
+        ];
+      };
+```
+
+### How to add a new Lean dependency to the project?
+
+Each `buildLeanPackage` can take a list of `deps`.
+
+Two cases:
+
+- either, this is a local dependency and this can be built like the `Base` (Aeneas standard library) one.
+- or, this is a remote dependency and this is often added to a Lakefile, this can be built like `Mathlib` and the others.
+
+## How to build?
+
+```console
+$ nix build .#docs
+```
+
+## How to deploy?
+
+The `result/` symlink is a HTML webroot, this can be deployed as a static website.
+
+## How to update the dependencies?
+
+You just updated `backends/lean/lakefile.lean` dependencies or the Lean version.
+
+### Lean version
+
+Update the flake URI in `flake.nix`, this will trigger a mass rebuild of the documentation: rebootstrapping Lean 4 (this may take a couple of minutes), rebuilding Mathlib4 (this may take up to 20 minutes on a fast computer), building Aeneas standard library and finally the documentation.
+
+### Updating Aeneas standard library's dependencies
+
+You may need to change all `hash = "...";` reference between `aeneas-base =` and `in`, which are the dependencies of `Base`, Aeneas standard library.
+
+To do so, you can replace `hash = "...";` by `hash = lib.fakeHash;`, and rebuild, i.e. `nix build .#doc`, Nix will provide the actual SRI hash.
+
+_Advice_ : build with `--keep-going` to get all hashes at once instead of having to copy one hash per one hash.
+
+## My build is failing due to a compilation error but it works outside of Nix
+
+This is highly likely due to a mismatch between the dependencies in the Nix setup and outside.
+
+The Nix setup reads the `lakefile-manifest.json`, but this lockfile is insufficient to lock purely the dependencies (NAR SHA256 serialization are missing).
+
+To overcome this, they are specified manually in `flake.nix`, but each time the Aeneas standard library updates their dependencies, the `flake.nix` needs to have all its hash rewritten. Refer to "How to update" for guidance.
+
+In the future, it could be smart to extend the lockfile format or write another file besides in the Aeneas standard library containing all NAR SHA256 serializations and link it in the Lake build system so that each updates would regenerate this file.
+
+# Reference documentation
+
+## `fetchFromLakeManifest`
+
+This is a simple Nix function that looks inside a Lean manifest and pulls the Git input information, it does not handle yet automatically fetching the NAR SHA256 serialization of the Git input as Lake does not store this information in its lockfile.
+
+This means that whenever you are updating the manifest, you need to replace all `hash = "...";` by `hash = lib.fakeHash;` to bust the cache, otherwise you will run into compilation errors.
+
+## `addFakeFiles`
+
+Mathlib4 depends on `proof-widgets`, a Lean library which depends on Node.js for its build system, to avoid wasting time to package multi-language dependency system, `addFakeFiles` is a function to poly-fill by **empty files** specific modules, fooling the build system into believing that these files have been built externally.
+
+## `renderPackage`
+
+This is a function to analyze an entire Lean package via [Alectryon](https://github.com/cpitclaudel/alectryon) and [LeanInk](https://github.com/leanprover/LeanInk) and assemble this as a tree of symlinks for each module in the package.
diff --git a/docs/user/TODO.md b/docs/user/TODO.md
new file mode 100644
index 000000000..a847e8da2
--- /dev/null
+++ b/docs/user/TODO.md
@@ -0,0 +1,8 @@
+# TODO list for this sub-project
+
+## Scaffolding
+
+This project makes use of the Lean flake, but this flake will be soon deprecated and be development-only.
+
+To overcome this problem, there's a need of https://github.com/oxalica/rust-overlay but for Lean, so that release candidates and various
+versions can be selected without a compilation cost by reusing Lean pre-built binaries, i.e. wrapping Lean binaries in FODs in that repository.
diff --git a/docs/user/alectryon.css b/docs/user/alectryon.css
new file mode 100644
index 000000000..6481909ef
--- /dev/null
+++ b/docs/user/alectryon.css
@@ -0,0 +1,786 @@
+@charset "UTF-8";
+/*
+Copyright © 2019 Clément Pit-Claudel
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
+*/
+
+/*******************************/
+/* CSS reset for .alectryon-io */
+/*******************************/
+
+.content {
+    /*
+    Use `initial` instead of `contents` to avoid a browser bug which removes
+    the element from the accessibility tree.
+    https://developer.mozilla.org/en-US/docs/Web/CSS/display#display_contents
+     */
+    display: initial;
+}
+
+.alectryon-io blockquote {
+    line-height: inherit;
+}
+
+.alectryon-io blockquote:after {
+    display: none;
+}
+
+.alectryon-io label {
+    display: inline;
+    font-size: inherit;
+    margin: 0;
+}
+
+.alectryon-io a {
+    text-decoration: none !important;
+    font-style: oblique !important;
+    color: unset;
+}
+
+/* Undo <small> and <blockquote>, added to improve RSS rendering. */
+
+.alectryon-io small.alectryon-output,
+.alectryon-io small.alectryon-type-info {
+    font-size: inherit;
+}
+
+.alectryon-io blockquote.alectryon-goal,
+.alectryon-io blockquote.alectryon-message {
+    font-weight: normal;
+    font-size: inherit;
+}
+
+/***************/
+/* Main styles */
+/***************/
+
+.alectryon-coqdoc .doc .code,
+.alectryon-coqdoc .doc .comment,
+.alectryon-coqdoc .doc .inlinecode,
+.alectryon-mref,
+.alectryon-block, .alectryon-io,
+.alectryon-toggle-label, .alectryon-banner {
+    font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace !important;
+    font-size: 0.875em;
+    font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
+    line-height: initial;
+}
+
+.alectryon-io, .alectryon-block, .alectryon-toggle-label, .alectryon-banner {
+    overflow: visible;
+    overflow-wrap: break-word;
+    position: relative;
+    white-space: pre-wrap;
+}
+
+/*
+CoqIDE doesn't turn off the unicode bidirectional algorithm (and PG simply
+respects the user's `bidi-display-reordering` setting), so don't turn it off
+here either.  But beware unexpected results like `Definition test_אב := 0.`
+
+.alectryon-io span {
+    direction: ltr;
+    unicode-bidi: bidi-override;
+}
+
+In any case, make an exception for comments:
+
+.highlight .c {
+    direction: embed;
+    unicode-bidi: initial;
+}
+*/
+
+.alectryon-mref,
+.alectryon-mref-marker {
+    align-self: center;
+    box-sizing: border-box;
+    display: inline-block;
+    font-size: 80%;
+    font-weight: bold;
+    line-height: 1;
+    box-shadow: 0 0 0 1pt black;
+    padding: 1pt 0.3em;
+    text-decoration: none;
+}
+
+.alectryon-block .alectryon-mref-marker,
+.alectryon-io .alectryon-mref-marker {
+    user-select: none;
+    margin: -0.25em 0 -0.25em 0.5em;
+}
+
+.alectryon-inline .alectryon-mref-marker {
+    margin: -0.25em 0.15em -0.25em 0.625em; /* 625 = 0.5em / 80% */
+}
+
+.alectryon-mref {
+    color: inherit;
+    margin: -0.5em 0.25em;
+}
+
+.alectryon-goal:target .goal-separator .alectryon-mref-marker,
+:target > .alectryon-mref-marker {
+    animation: blink 0.2s step-start 0s 3 normal none;
+    background-color: #fcaf3e;
+    position: relative;
+}
+
+@keyframes blink {
+    50% {
+        box-shadow: 0 0 0 3pt #fcaf3e, 0 0 0 4pt black;
+        z-index: 10;
+    }
+}
+
+.alectryon-toggle,
+.alectryon-io .alectryon-extra-goal-toggle {
+    display: none;
+}
+
+.alectryon-bubble,
+.alectryon-io label,
+.alectryon-toggle-label {
+    cursor: pointer;
+}
+
+.alectryon-toggle-label {
+    display: block;
+    font-size: 0.8em;
+}
+
+.alectryon-io .alectryon-input {
+    padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */
+}
+
+.alectryon-io .alectryon-token {
+    white-space: pre-wrap;
+    display: inline;
+}
+
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-input {
+    /* FIXME if keywords were ‘bolder’ we wouldn't need !important */
+    font-weight: bold !important; /* Use !important to avoid a * selector */
+}
+
+.alectryon-bubble:before,
+.alectryon-toggle-label:before,
+.alectryon-io label.alectryon-input:after,
+.alectryon-io .alectryon-goal > label:before {
+    border: 1px solid #babdb6;
+    border-radius: 1em;
+    box-sizing: border-box;
+    content: '';
+    display: inline-block;
+    font-weight: bold;
+    height: 0.25em;
+    margin-bottom: 0.15em;
+    vertical-align: middle;
+    width: 0.75em;
+}
+
+.alectryon-toggle-label:before,
+.alectryon-io .alectryon-goal > label:before {
+    margin-right: 0.25em;
+}
+
+.alectryon-io .alectryon-goal > label:before {
+    margin-top: 0.125em;
+}
+
+.alectryon-io label.alectryon-input {
+    padding-right: 1em; /* Prevent line wraps before the checkbox bubble */
+}
+
+.alectryon-io label.alectryon-input:after {
+    margin-left: 0.25em;
+    margin-right: -1em; /* Compensate for the anti-wrapping space */
+}
+
+.alectryon-failed {
+    /* Underlines are broken in Chrome (they reset at each element boundary)… */
+    /* text-decoration: red wavy underline; */
+    /* … but it isn't too noticeable with dots */
+    text-decoration: red dotted underline;
+    text-decoration-skip-ink: none;
+    /* Chrome prints background images in low resolution, yielding a blurry underline */
+    /* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
+}
+
+/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence
+   doesn't trigger its :hover state (otherwise, on mobile, tapping a sentence to
+   hide its output causes it to remain visible (its :hover state gets triggered.
+   We only do it for the default style though, since other styles don't put the
+   output over the main text, so showing too much is not an issue. */
+@media (any-hover: hover) {
+    .alectryon-bubble:hover:before,
+    .alectryon-toggle-label:hover:before,
+    .alectryon-io label.alectryon-input:hover:after {
+        background: #eeeeec;
+    }
+
+    .alectryon-io label.alectryon-input:hover {
+        text-decoration: underline dotted #babdb6;
+	    text-shadow: 0 0 1px rgb(46, 52, 54, 0.3); /* #2e3436 + opacity */
+    }
+
+    .alectryon-io .alectryon-sentence:hover .alectryon-output,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {
+        z-index: 2; /* Place hovered goals above .alectryon-sentence.alectryon-target ones */
+    }
+}
+
+.alectryon-toggle:checked + .alectryon-toggle-label:before,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked + label.alectryon-input:after,
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal > label:before {
+    background-color: #babdb6;
+    border-color: #babdb6;
+}
+
+/* Disable clicks on sentences when the document-wide toggle is set. */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input {
+    cursor: unset;
+    pointer-events: none;
+}
+
+/* Hide individual checkboxes when the document-wide toggle is set. */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input:after {
+    display: none;
+}
+
+/* .alectryon-output is displayed by toggles, :hover, and .alectryon-target rules */
+.alectryon-io .alectryon-output {
+    box-sizing: border-box;
+    display: none;
+    left: 0;
+    right: 0;
+    position: absolute;
+    padding: 0.25em 0;
+    overflow: visible; /* Let box-shadows overflow */
+    z-index: 1; /* Default to an index lower than that used by :hover */
+}
+
+.alectryon-io .alectryon-type-info-wrapper {
+    position: absolute;
+    display: inline-block;
+    width: 100%;
+}
+
+.alectryon-io .alectryon-type-info-wrapper.full-width {
+    left: 0;
+    min-width: 100%;
+    max-width: 100%;
+}
+
+.alectryon-io .alectryon-type-info .goal-separator {
+    height: unset;
+    margin-top: 0em;
+}
+
+.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info {
+    box-sizing: border-box;
+    bottom: 100%;
+    position: absolute;
+    /*padding: 0.25em 0;*/
+    visibility: hidden;
+    overflow: visible; /* Let box-shadows overflow */
+    z-index: 1; /* Default to an index lower than that used by :hover */
+    white-space: pre-wrap !important;
+}
+
+.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info .alectryon-goal.alectryon-docstring {
+    white-space: pre-wrap !important;
+}
+
+@media (any-hover: hover) { /* See note above about this @media query */
+    .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) {
+        display: block;
+    }
+
+    .alectryon-io.output-hidden .alectryon-sentence:hover .alectryon-output:not(:hover) {
+        display: none !important;
+    }
+
+    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
+    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+        /*visibility: hidden !important;*/
+    }
+
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+        visibility: visible;
+        transition-delay: 0.5s;
+    }
+}
+
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output {
+    display: block;
+}
+
+/* Indicate active (hovered or targeted) goals with a shadow. */
+.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
+.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals,
+.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+    box-shadow: 2px 2px 2px gray;
+}
+
+.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-hyps {
+    display: none;
+}
+
+.alectryon-io .alectryon-extra-goals .alectryon-extra-goal-toggle:not(:checked) + .alectryon-goal label.goal-separator hr {
+    /* Dashes indicate that the hypotheses are hidden */
+    border-top-style: dashed;
+}
+
+
+/* Show just a small preview of the other goals; this is undone by the
+   "extra-goal" toggle and by :hover and .alectryon-target in windowed mode. */
+.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-conclusion {
+    max-height: 5.2em;
+    overflow-y: auto;
+    /* Combining ‘overflow-y: auto’ with ‘display: inline-block’ causes extra space
+       to be added below the box. ‘vertical-align: middle’ gets rid of it. */
+    vertical-align: middle;
+}
+
+.alectryon-io .alectryon-goals,
+.alectryon-io .alectryon-messages {
+    background: #f6f7f6;
+	/*border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */
+    display: block;
+    padding: 0.25em;
+}
+
+.alectryon-message::before {
+    content: '';
+    float: right;
+    /* etc/svg/square-bubble-xl.svg */
+    background: url("data:image/svg+xml,%3Csvg width='14' height='14' viewBox='0 0 3.704 3.704' xmlns='http://www.w3.org/2000/svg'%3E%3Cg fill-rule='evenodd' stroke='%23000' stroke-width='.264'%3E%3Cpath d='M.794.934h2.115M.794 1.463h1.455M.794 1.992h1.852'/%3E%3C/g%3E%3Cpath d='M.132.14v2.646h.794v.661l.926-.661h1.72V.14z' fill='none' stroke='%23000' stroke-width='.265'/%3E%3C/svg%3E") top right no-repeat;
+    height: 14px;
+    width: 14px;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container {
+    width: unset;
+}
+
+/* Show goals when a toggle is set */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output {
+    display: block;
+    position: static;
+    width: unset;
+    background: unset; /* Override the backgrounds set in floating in windowed mode */
+    padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */
+}
+
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output .goal-hyps {
+    /* Overridden back in windowed style */
+    flex-flow: row wrap;
+    justify-content: flex-start;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
+    display: block;
+}
+
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-hyps {
+    display: flex;
+}
+
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion {
+    max-height: unset;
+    overflow-y: unset;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence > .alectryon-toggle ~ .alectryon-wsp,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-wsp {
+    display: none;
+}
+
+.alectryon-io .alectryon-messages,
+.alectryon-io .alectryon-message,
+.alectryon-io .alectryon-goals,
+.alectryon-io .alectryon-goal,
+.alectryon-io .goal-hyps > span,
+.alectryon-io .goal-conclusion {
+    border-radius: 0.15em;
+}
+
+.alectryon-io .alectryon-goal,
+.alectryon-io .alectryon-message {
+    align-items: center;
+    background: #f6f7f6;
+    border: 0em;
+    display: block;
+    flex-direction: column;
+    margin: 0.25em;
+    padding: 0.5em;
+    position: relative;
+}
+
+.alectryon-io .goal-hyps {
+    align-content: space-around;
+    align-items: baseline;
+    display: flex;
+    flex-flow: column nowrap; /* re-stated in windowed mode */
+    justify-content: space-around;
+    /* LATER use a ‘gap’ property instead of margins once supported */
+    margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */
+    padding-bottom: 0.35em; /* 0.5em-0.15em to cancel the 0.5em of .goal-separator */
+}
+
+.alectryon-io .goal-hyps > br {
+    display: none; /* Only for RSS readers */
+}
+
+.alectryon-io .goal-hyps > span,
+.alectryon-io .goal-conclusion {
+    /*background: #eeeeec;*/
+    display: inline-block;
+    padding: 0.15em 0.35em;
+}
+
+.alectryon-io .goal-hyps > span {
+    align-items: baseline;
+    display: inline-flex;
+    margin: 0.15em 0.25em;
+}
+
+.alectryon-block var,
+.alectryon-inline var,
+.alectryon-io .goal-hyps > span > var {
+    font-weight: 600;
+    font-style: unset;
+}
+
+.alectryon-io .goal-hyps > span > var {
+    /* Shrink the list of names, but let it grow as long as space is available. */
+    flex-basis: min-content;
+    flex-grow: 1;
+}
+
+.alectryon-io .goal-hyps > span b {
+    font-weight: 600;
+    margin: 0 0 0 0.5em;
+    white-space: pre;
+}
+
+.alectryon-io .hyp-body,
+.alectryon-io .hyp-type {
+    display: flex;
+    align-items: baseline;
+}
+
+.alectryon-io .goal-separator {
+    align-items: center;
+    display: flex;
+    flex-direction: row;
+    height: 1em; /* Fixed height to ignore goal name and markers */
+    margin-top: -0.5em; /* Compensated in .goal-hyps when shown */
+}
+
+.alectryon-io .goal-separator hr {
+    border: none;
+    border-top: thin solid #555753;
+    display: block;
+    flex-grow: 1;
+    margin: 0;
+}
+
+.alectryon-io .goal-separator .goal-name {
+    font-size: 0.75em;
+    margin-left: 0.5em;
+}
+
+/**********/
+/* Banner */
+/**********/
+
+.alectryon-banner {
+    background: #eeeeec;
+    border: 1px solid #babcbd;
+    font-size: 0.75em;
+    padding: 0.25em;
+    text-align: center;
+    margin: 1em 0;
+}
+
+.alectryon-banner a {
+    cursor: pointer;
+    text-decoration: underline;
+}
+
+.alectryon-banner kbd {
+    background: #d3d7cf;
+    border-radius: 0.15em;
+    border: 1px solid #babdb6;
+    box-sizing: border-box;
+    display: inline-block;
+    font-family: inherit;
+    font-size: 0.9em;
+    height: 1.3em;
+    line-height: 1.2em;
+    margin: -0.25em 0;
+    padding: 0 0.25em;
+    vertical-align: middle;
+}
+
+/**********/
+/* Toggle */
+/**********/
+
+.alectryon-toggle-label {
+    margin: 1rem 0;
+}
+
+/******************/
+/* Floating style */
+/******************/
+
+/* If there's space, display goals to the right of the code, not below it. */
+@media (min-width: 80rem) {
+    /* Unlike the windowed case, we don't want to move output blocks to the side
+       when they are both :checked and -targeted, since it gets confusing as
+       things jump around; hence the commented-output part of the selector,
+       which would otherwise increase specificity */
+    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output,
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
+        top: 0;
+        left: 100%;
+        right: -100%;
+        padding: 0 0.5em;
+        position:  absolute;
+    }
+
+    .alectryon-floating .alectryon-output {
+        min-height: 100%;
+    }
+
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
+        background: white; /* Ensure that short goals hide long ones */
+    }
+
+    /* This odd margin-bottom property prevents the sticky div from bumping
+       against the bottom of its container (.alectryon-output).  The alternative
+       would be enlarging .alectryon-output, but that would cause overflows,
+       enlarging scrollbars and yielding scrolling towards the bottom of the
+       page.  Doing things this way instead makes it possible to restrict
+       .alectryon-output to a reasonable size (100%, through top = bottom = 0).
+       See also https://stackoverflow.com/questions/43909940/. */
+    /* See note on specificity above */
+    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output > div,
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output > div {
+        margin-bottom: -200%;
+        position: sticky;
+        top: 0;
+    }
+
+    .alectryon-floating .alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
+    .alectryon-floating .alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
+        margin-bottom: unset; /* Undo the margin */
+    }
+
+    /* Float underneath the current fragment
+    @media (max-width: 80rem) {
+        .alectryon-floating .alectryon-output {
+            top: 100%;
+        }
+    } */
+}
+
+/********************/
+/* Multi-pane style */
+/********************/
+
+.alectryon-windowed {
+    border: 0 solid #2e3436;
+    box-sizing: border-box;
+}
+
+.alectryon-windowed .alectryon-sentence:hover .alectryon-output {
+    background: white; /* Ensure that short goals hide long ones */
+}
+
+.alectryon-windowed .alectryon-output {
+    position: fixed; /* Overwritten by the ‘:checked’ rules */
+}
+
+/* See note about specificity below */
+.alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
+    padding: 0.5em;
+    overflow-y: auto; /* Windowed contents may need to scroll */
+}
+
+.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
+.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals {
+    box-shadow: none; /* A shadow is unnecessary here and incompatible with overflow-y set to auto */
+}
+
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .goal-hyps {
+    /* Restated to override the :checked style */
+    flex-flow: column nowrap;
+    justify-content: space-around;
+}
+
+
+.alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-extra-goals .alectryon-goal .goal-conclusion
+/* Like .alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion */ {
+    max-height: unset;
+    overflow-y: unset;
+}
+
+.alectryon-windowed .alectryon-output > div {
+    display: flex; /* Put messages after goals */
+    flex-direction: column-reverse;
+}
+
+/*********************/
+/* Standalone styles */
+/*********************/
+
+.alectryon-standalone {
+    font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
+    line-height: 1.5;
+}
+
+@media screen and (min-width: 50rem) {
+    html.alectryon-standalone {
+        /* Prevent flickering when hovering a block causes scrollbars to appear. */
+        margin-left: calc(100vw - 100%);
+        margin-right: 0;
+    }
+}
+
+/* Coqdoc */
+
+.alectryon-coqdoc .doc .code,
+.alectryon-coqdoc .doc .inlinecode,
+.alectryon-coqdoc .doc .comment {
+    display: inline;
+}
+
+.alectryon-coqdoc .doc .comment {
+    color: #eeeeec;
+}
+
+.alectryon-coqdoc .doc .paragraph {
+    height: 0.75em;
+}
+
+/* Centered, Floating */
+
+.alectryon-standalone .alectryon-centered,
+.alectryon-standalone .alectryon-floating {
+    max-width: 50rem;
+    margin: auto;
+}
+
+@media (min-width: 80rem) {
+    .alectryon-standalone .alectryon-floating {
+        max-width: 80rem;
+    }
+
+    .alectryon-standalone .alectryon-floating > * {
+        width: 50%;
+        margin-left: 0;
+    }
+}
+
+/* Windowed */
+
+.alectryon-standalone .alectryon-windowed {
+    display: block;
+    margin: 0;
+    overflow-y: auto;
+    position: absolute;
+    padding: 0 1em;
+}
+
+.alectryon-standalone .alectryon-windowed > * {
+    /* Override properties of docutils_basic.css */
+    margin-left: 0;
+    max-width: unset;
+}
+
+.alectryon-standalone .alectryon-windowed .alectryon-io {
+    box-sizing: border-box;
+    width: 100%;
+}
+
+/* No need to predicate the ‘:hover’ rules below on ‘:not(:checked)’, since ‘left’,
+   ‘right’, ‘top’, and ‘bottom’ will be inactived by the :checked rules setting
+   ‘position’ to ‘static’ */
+
+
+/* Specificity: We want the output to stay inline when hovered while unfolded
+   (:checked), but we want it to move when it's targeted (i.e. when the user
+   is browsing goals one by one using the keyboard, in which case we want to
+   goals to appear in consistent locations).  The selectors below ensure
+   that :hover < :checked < -targeted in terms of specificity. */
+/* LATER: Reimplement this stuff with CSS variables */
+.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
+    position: fixed;
+}
+
+@media screen and (min-width: 60rem) {
+    .alectryon-standalone .alectryon-windowed {
+        border-right-width: thin;
+        bottom: 0;
+        left: 0;
+        right: 50%;
+        top: 0;
+    }
+
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
+        bottom: 0;
+        left: 50%;
+        right: 0;
+        top: 0;
+    }
+}
+
+@media screen and (max-width: 60rem) {
+    .alectryon-standalone .alectryon-windowed {
+        border-bottom-width: 1px;
+        bottom: 40%;
+        left: 0;
+        right: 0;
+        top: 0;
+    }
+
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
+        bottom: 0;
+        left: 0;
+        right: 0;
+        top: 60%;
+    }
+}
diff --git a/docs/user/alectryon.js b/docs/user/alectryon.js
new file mode 100644
index 000000000..d503e0fd2
--- /dev/null
+++ b/docs/user/alectryon.js
@@ -0,0 +1,190 @@
+var Alectryon;
+(function(Alectryon) {
+    (function (slideshow) {
+        function anchor(sentence) { return "#" + sentence.id; }
+
+        function current_sentence() { return slideshow.sentences[slideshow.pos]; }
+
+        function unhighlight() {
+            var sentence = current_sentence();
+            if (sentence) sentence.classList.remove("alectryon-target");
+            slideshow.pos = -1;
+        }
+
+        function highlight(sentence) {
+            sentence.classList.add("alectryon-target");
+        }
+
+        function scroll(sentence) {
+            // Put the top of the current fragment close to the top of the
+            // screen, but scroll it out of view if showing it requires pushing
+            // the sentence past half of the screen.  If sentence is already in
+            // a reasonable position, don't move.
+            var parent = sentence.parentElement;
+            /* We want to scroll the whole document, so start at root… */
+            while (parent && !parent.classList.contains("alectryon-root"))
+                parent = parent.parentElement;
+            /* … and work up from there to find a scrollable element.
+               parent.scrollHeight can be greater than parent.clientHeight
+               without showing scrollbars, so we add a 10px buffer. */
+            while (parent && parent.scrollHeight <= parent.clientHeight + 10)
+                parent = parent.parentElement;
+            /* <body> and <html> elements can have their client rect overflow
+             * the window if their height is unset, so scroll the window
+             * instead */
+            if (parent && (parent.nodeName == "BODY" || parent.nodeName == "HTML"))
+                parent = null;
+
+            var rect = function(e) { return e.getBoundingClientRect(); };
+            var parent_box = parent ? rect(parent) : { y: 0, height: window.innerHeight },
+                sentence_y = rect(sentence).y - parent_box.y,
+                fragment_y = rect(sentence.parentElement).y - parent_box.y;
+
+            // The assertion below sometimes fails for the first element in a block.
+            // console.assert(sentence_y >= fragment_y);
+
+            if (sentence_y < 0.1 * parent_box.height ||
+                sentence_y > 0.7 * parent_box.height) {
+                (parent || window).scrollBy(
+                    0, Math.max(sentence_y - 0.5 * parent_box.height,
+                                fragment_y - 0.1 * parent_box.height));
+            }
+        }
+
+        function highlighted(pos) {
+            return slideshow.pos == pos;
+        }
+
+        function navigate(pos, inhibitScroll) {
+            unhighlight();
+            slideshow.pos = Math.min(Math.max(pos, 0), slideshow.sentences.length - 1);
+            var sentence = current_sentence();
+            highlight(sentence);
+            if (!inhibitScroll)
+                scroll(sentence);
+        }
+
+        var keys = {
+            PAGE_UP: 33,
+            PAGE_DOWN: 34,
+            ARROW_UP: 38,
+            ARROW_DOWN: 40,
+            h: 72, l: 76, p: 80, n: 78
+        };
+
+        function onkeydown(e) {
+            e = e || window.event;
+            if (e.ctrlKey || e.metaKey) {
+                if (e.keyCode == keys.ARROW_UP)
+                    slideshow.previous();
+                else if (e.keyCode == keys.ARROW_DOWN)
+                    slideshow.next();
+                else
+                    return;
+            } else {
+                // if (e.keyCode == keys.PAGE_UP || e.keyCode == keys.p || e.keyCode == keys.h)
+                //     slideshow.previous();
+                // else if (e.keyCode == keys.PAGE_DOWN || e.keyCode == keys.n || e.keyCode == keys.l)
+                //     slideshow.next();
+                // else
+                return;
+            }
+            e.preventDefault();
+        }
+
+        function start() {
+            slideshow.navigate(0);
+        }
+
+        function toggleHighlight(idx) {
+            if (highlighted(idx))
+                unhighlight();
+            else
+                navigate(idx, true);
+        }
+
+        function handleClick(evt) {
+            if (evt.ctrlKey || evt.metaKey) {
+                var sentence = evt.currentTarget;
+
+                // Ensure that the goal is shown on the side, not inline
+                var checkbox = sentence.getElementsByClassName("alectryon-toggle")[0];
+                if (checkbox)
+                    checkbox.checked = false;
+
+                toggleHighlight(sentence.alectryon_index);
+                evt.preventDefault();
+            }
+        }
+
+        function init() {
+            document.onkeydown = onkeydown;
+            slideshow.pos = -1;
+            slideshow.sentences = Array.from(document.getElementsByClassName("alectryon-sentence"));
+            slideshow.sentences.forEach(function (s, idx) {
+                s.addEventListener('click', handleClick, false);
+                s.alectryon_index = idx;
+            });
+        }
+
+        slideshow.start = start;
+        slideshow.end = unhighlight;
+        slideshow.navigate = navigate;
+        slideshow.next = function() { navigate(slideshow.pos + 1); };
+        slideshow.previous = function() { navigate(slideshow.pos + -1); };
+        window.addEventListener('DOMContentLoaded', init);
+    })(Alectryon.slideshow || (Alectryon.slideshow = {}));
+
+    (function (styles) {
+        var styleNames = ["centered", "floating", "windowed"];
+
+        function className(style) {
+            return "alectryon-" + style;
+        }
+
+        function setStyle(style) {
+            var root = document.getElementsByClassName("alectryon-root")[0];
+            styleNames.forEach(function (s) {
+                root.classList.remove(className(s)); });
+            root.classList.add(className(style));
+        }
+
+        function init() {
+            var banner = document.getElementsByClassName("alectryon-banner")[0];
+            if (banner) {
+                banner.append(" Style: ");
+                styleNames.forEach(function (styleName, idx) {
+                    var s = styleName;
+                    var a = document.createElement("a");
+                    a.onclick = function() { setStyle(s); };
+                    a.append(styleName);
+                    if (idx > 0) banner.append("; ");
+                    banner.appendChild(a);
+                });
+                banner.append(".");
+            }
+        }
+
+        window.addEventListener('DOMContentLoaded', init);
+
+        styles.setStyle = setStyle;
+    })(Alectryon.styles || (Alectryon.styles = {}));
+})(Alectryon || (Alectryon = {}));
+
+function setHidden(elements, isVisible, token) {
+    for (let i = 0; i < elements.length; i++) {
+        if (isVisible) {
+            elements[i].classList.remove(token)
+        } else {
+            elements[i].classList.add(token)
+        }
+    }
+}
+
+function toggleShowTypes(checkbox) {
+    setHidden(document.getElementsByClassName("alectryon-io"), checkbox.checked, "type-info-hidden")
+}
+
+function toggleShowGoals(checkbox) {
+    setHidden(document.getElementsByClassName("alectryon-io"), checkbox.checked, "output-hidden")
+}
\ No newline at end of file
diff --git a/docs/user/book.toml b/docs/user/book.toml
index 333659cba..5f5457b6b 100644
--- a/docs/user/book.toml
+++ b/docs/user/book.toml
@@ -4,3 +4,15 @@ language = "en"
 multilingual = false
 src = "src"
 title = "Aeneas user documentation"
+
+[output.html]
+mathjax-support = true
+additional-css = ["alectryon.css", "pygments.css"]
+additional-js = ["alectryon.js"]
+
+[output.html.fold]
+enable = true
+level = 0
+
+[output.html.playground.boring-prefixes]
+lean = "# "
diff --git a/docs/user/flake.lock b/docs/user/flake.lock
index dfd3938b6..cdc9b610c 100644
--- a/docs/user/flake.lock
+++ b/docs/user/flake.lock
@@ -17,22 +17,6 @@
         "type": "github"
       }
     },
-    "flake-compat": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1673956053,
-        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
-        "owner": "edolstra",
-        "repo": "flake-compat",
-        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
-        "type": "github"
-      },
-      "original": {
-        "owner": "edolstra",
-        "repo": "flake-compat",
-        "type": "github"
-      }
-    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"
@@ -54,41 +38,24 @@
     "lean": {
       "inputs": {
         "flake-utils": "flake-utils",
-        "lean4-mode": "lean4-mode",
-        "nix": "nix",
-        "nixpkgs": "nixpkgs_2",
+        "nixpkgs": "nixpkgs",
         "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
-        "lastModified": 1720529829,
-        "narHash": "sha256-hPqn4qRfe7bLAaNRvK1RDC50IUuCaxDCcv5NtNsETEQ=",
+        "lastModified": 1723429404,
+        "narHash": "sha256-Us3VccCsU1nsqMtAuG5hUYR95j7a8/dQqtBpQE4Cgb0=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "f531f4e5db8f402a015a69373af9a002fe754acd",
+        "rev": "0edf1bac392f7e2fe0266b28b51c498306363a84",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
+        "ref": "v4.11.0-rc2",
         "repo": "lean4",
         "type": "github"
       }
     },
-    "lean4-mode": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1709737301,
-        "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=",
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f",
-        "type": "github"
-      },
-      "original": {
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "type": "github"
-      }
-    },
     "leanInk": {
       "flake": false,
       "locked": {
@@ -105,22 +72,6 @@
         "type": "github"
       }
     },
-    "libgit2": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1697646580,
-        "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=",
-        "owner": "libgit2",
-        "repo": "libgit2",
-        "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5",
-        "type": "github"
-      },
-      "original": {
-        "owner": "libgit2",
-        "repo": "libgit2",
-        "type": "github"
-      }
-    },
     "mdBook": {
       "flake": false,
       "locked": {
@@ -137,39 +88,18 @@
         "type": "github"
       }
     },
-    "nix": {
-      "inputs": {
-        "flake-compat": "flake-compat",
-        "libgit2": "libgit2",
-        "nixpkgs": "nixpkgs",
-        "nixpkgs-regression": "nixpkgs-regression"
-      },
-      "locked": {
-        "lastModified": 1711102798,
-        "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=",
-        "owner": "NixOS",
-        "repo": "nix",
-        "rev": "a22328066416650471c3545b0b138669ea212ab4",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nix",
-        "type": "github"
-      }
-    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1709083642,
-        "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=",
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "b550fe4b4776908ac2a861124307045f8e717c8e",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
-        "ref": "release-23.11",
+        "ref": "nixpkgs-unstable",
         "repo": "nixpkgs",
         "type": "github"
       }
@@ -191,38 +121,6 @@
         "type": "github"
       }
     },
-    "nixpkgs-regression": {
-      "locked": {
-        "lastModified": 1643052045,
-        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "github"
-      }
-    },
-    "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1710889954,
-        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixpkgs-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
     "root": {
       "inputs": {
         "alectryon": "alectryon",
diff --git a/docs/user/flake.nix b/docs/user/flake.nix
index be1576145..ce1de65c6 100644
--- a/docs/user/flake.nix
+++ b/docs/user/flake.nix
@@ -2,7 +2,8 @@
 {
   description = "Aeneas documentation";
 
-  inputs.lean.url = "github:leanprover/lean4";
+  # When you update Lean in Aeneas, update this URI as well.
+  inputs.lean.url = "github:leanprover/lean4/v4.11.0-rc2";
   inputs.flake-utils.follows = "lean/flake-utils";
   inputs.mdBook = {
     url = "github:leanprover/mdBook";
@@ -18,9 +19,10 @@
   };
 
   outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system:
-    with inputs.lean.packages.${system}; with nixpkgs;
+    with inputs.lean.packages.${system}.deprecated; with nixpkgs;
     let
       doc-src = ./.; # lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"];
+      leanLib = callPackage ./nix { };
     in {
     packages = rec {
       lean-mdbook = mdbook.overrideAttrs (drv: rec {
@@ -32,32 +34,24 @@
         });
         doCheck = false;
       });
+
+      # This is the final book:
+      # * We copy the classical mdBook contents.
+      # * We interpose the inked Lean files (*.lean.md) in the source tree
+      # Finally, we call mdBook to process this soup into a HTML webroot you can deploy.
       book = stdenv.mkDerivation {
         name = "aeneas-doc";
         src = doc-src;
         buildInputs = [ lean-mdbook ];
         buildCommand = ''
+          set -x
           mkdir $out
           # necessary for `additional-css`...?
           cp -vr --no-preserve=mode $src/* .
+          cp -vr --no-preserve=mode ${inked.out}/* .
           mdbook build -d $out
         '';
       };
-      # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache
-      test = stdenv.mkDerivation {
-        name = "aeneas-doc-test";
-        src = doc-src;
-        buildInputs = [ lean-mdbook stage1.Lean.lean-package strace ];
-        patchPhase = ''
-          cd doc
-          patchShebangs test
-        '';
-        buildPhase = ''
-          mdbook test
-          touch $out
-        '';
-        dontInstall = true;
-      };
 
       leanInk = (buildLeanPackage {
         name = "Main";
@@ -97,14 +91,128 @@
         paths = map renderLeanMod (lib.attrValues pkg.mods);
       };
 
+      aeneas-base = 
+      let
+        manifest = builtins.fromJSON (builtins.readFile ../../backends/lean/lake-manifest.json);
+        fetchFromLakeManifest = leanLib.fetchFromLakeManifest manifest;
+        inherit (leanLib) addFakeFiles;
+
+        # To update the dependencies, just ensure that the `lake-manifest.json`
+        # in `backends/lean` is up to date. Then, replace each `hash = "...";`
+        # by `hash = lib.fakeHash;` Then, perform `nix build .#doc
+        # --keep-going` to get all the new hashes. Copy them back here and
+        # commit this result.
+
+        # Those are specifically the Mathlib4 dependencies.
+        batteries = buildLeanPackage {
+          name = "Batteries";
+          src = fetchFromLakeManifest {
+            name = "batteries";
+            hash = "sha256-EGcjOcTu66rtAICAqgPKaR8kBlImoq4lUZfNZR9dHiY=";
+          };
+        };
+        qq = buildLeanPackage {
+          name = "Qq";
+          src = fetchFromLakeManifest {
+            name = "Qq";
+            hash = "sha256-iFlAiq8Uxq+QD6ql4EMpRQENvIhKdioaleoEiDmMuDQ=";
+          };
+        };
+        aesop = buildLeanPackage {
+          name = "Aesop";
+          deps = [ batteries ];
+          src = fetchFromLakeManifest {
+            name = "aesop";
+            hash = "sha256-97xcl82SU9/EZ8L4vT7g/Ureoi11s3c4ZeFlaCd4Az4=";
+          };
+        };
+        import-graph = buildLeanPackage {
+          name = "ImportGraph";
+          deps = [ batteries ];
+          src = fetchFromLakeManifest {
+            name = "importGraph";
+            hash = "sha256-u8tk5IWU/n47kmNAlxZCmurq7e08oCzANhsk9VJeCCM=";
+          };
+        };
+        proof-widgets = buildLeanPackage {
+          name = "ProofWidgets";
+          deps = [ batteries ];
+          src = fetchFromLakeManifest {
+            name = "proofwidgets";
+            hash = "sha256-jPvUi73NylxFiU5V0tjK92M0hJfHWZi5ULZldDwctYY=";
+          };
+
+          # ProofWidgets require a special Node.js build pass encoded in its
+          # Lakefile In principle, we could parse the Node.js lockfile, lock it
+          # using Nix, generate these JS files and link them properly in the
+          # build process. But we make no use of ProofWidgets in Aeneas manual,
+          # so we just polyfill all of these files by empty files, satisfying
+          # Lake build process.
+          overrideBuildModAttrs = addFakeFiles {
+            "ProofWidgets.Compat" = [ ".lake/build/js/compat.js" ];
+            "ProofWidgets.Component.Basic" = [ ".lake/build/js/interactiveExpr.js" ];
+            "ProofWidgets.Component.GoalTypePanel" = [ ".lake/build/js/goalTypePanel.js" ];
+            "ProofWidgets.Component.Recharts" = [ ".lake/build/js/recharts.js" ];
+            "ProofWidgets.Component.PenroseDiagram" = [ ".lake/build/js/penroseDisplay.js" ];
+            "ProofWidgets.Component.Panel.SelectionPanel" = [ ".lake/build/js/presentSelection.js" ];
+            "ProofWidgets.Component.Panel.GoalTypePanel" = [ ".lake/build/js/goalTypePanel.js" ];
+            "ProofWidgets.Component.MakeEditLink" = [ ".lake/build/js/makeEditLink.js" ];
+            "ProofWidgets.Component.OfRpcMethod" = [ ".lake/build/js/ofRpcMethod.js" ];
+            "ProofWidgets.Component.FilterDetails" = [ ".lake/build/js/filterDetails.js" ];
+            "ProofWidgets.Component.HtmlDisplay" =
+              [ ".lake/build/js/htmlDisplay.js" ".lake/build/js/htmlDisplayPanel.js"];
+              "ProofWidgets.Presentation.Expr" = [ ".lake/build/js/exprPresentation.js" ];
+          };
+        };
+        # This is Mathlib4, a dependency of Aeneas standard library.
+        mathlib = buildLeanPackage {
+          deps = [ qq aesop batteries import-graph proof-widgets ];
+          name = "Mathlib";
+          src = fetchFromLakeManifest {
+            name = "mathlib";
+            hash = "sha256-3FnWd0dUVhNyUPxLNNHA41RWF34fwmXulnRSIEmIQXM=";
+          };
+        };
+      in
+      # Aeneas standard library does not require any hashing
+      # as it is present in this local repository.
+      buildLeanPackage {
+        name = "Base";
+        deps = [ mathlib ];
+        src = ../../backends/lean;
+      };
+
+      # This is a meta Lean package of all Lean files used in the documentation.
       literate = buildLeanPackage {
         name = "literate";
+        # Add here new Lean packages if you need them for the manual
+        deps = [ aeneas-base ];
         src = ./.;
-        roots = [ ];
+        # To add a new directory containing Lean files to be processed
+        # by Alectryon, add a new attribute set `{ mod = "path to the lean files"; glob = "submodules"; }`
+        roots = [
+          {
+            mod = "src/lean/basics";
+            glob = "submodules";
+          }
+        ];
       };
+
+      # This is the tree of all inked Lean files, i.e. the *.lean.md files
+      # expected by mdBook.
       inked = renderPackage literate;
+
+      # This is the final book.
       doc = book;
     };
     defaultPackage = self.packages.${system}.doc;
+    devShells.default = mkShell {
+      packages = [
+        # If you need to run Alectryon or LeanInk manually for tests
+        # This is available in the default development shell.
+        self.packages.${system}.alectryon
+        self.packages.${system}.leanInk
+      ];
+    };
   });
 }
diff --git a/docs/user/lake-manifest.json b/docs/user/lake-manifest.json
new file mode 100644
index 000000000..f30016c59
--- /dev/null
+++ b/docs/user/lake-manifest.json
@@ -0,0 +1,82 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "cf30d04b6448dbb5a5b30a7d031e3949e74b9dd1",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.39",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e242f1edcacf917f40fae9b81f57f4bd0a4e45ac",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "base",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../../backends/lean",
+   "configFile": "lakefile.lean"}],
+ "name": "Manual",
+ "lakeDir": ".lake"}
diff --git a/docs/user/lakefile.lean b/docs/user/lakefile.lean
new file mode 100644
index 000000000..fef1b0abd
--- /dev/null
+++ b/docs/user/lakefile.lean
@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+require base from "../../backends/lean"
+
+package «Manual» where
+  -- add package configuration options here
diff --git a/docs/user/lean-toolchain b/docs/user/lean-toolchain
new file mode 100644
index 000000000..6a4259fa5
--- /dev/null
+++ b/docs/user/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.10.0-rc2
diff --git a/docs/user/nix/default.nix b/docs/user/nix/default.nix
new file mode 100644
index 000000000..b90dda26b
--- /dev/null
+++ b/docs/user/nix/default.nix
@@ -0,0 +1,37 @@
+{ emptyFile, runCommandCC, lib, callPackage, ... }: {
+  /* Given a parsed Lake manifest in Nix,
+    this will fetch a specific Lake dependency of the manifest.
+
+    This currently only supports Git inputs.
+  */
+  fetchFromLakeManifest = manifest: { name, hash, ... }:
+  let 
+    dep = lib.findFirst (pkg: pkg.name == name) null manifest.packages;
+  in 
+  assert dep != null;
+  assert dep.type == "git"; fetchGit {
+    inherit (dep) url rev;
+    narHash = hash;
+  } // (if dep.inputRev != null then { ref = dep.inputRev; } else {});
+
+  # Inspired from Loogle scaffolding.
+  # addFakeFile can plug into buildLeanPackage’s overrideBuildModAttrs
+  # it takes a lean module name and a filename, and makes that file available
+  # (as an empty file) in the build tree, e.g. for include_str.
+  addFakeFiles = m: self: super:
+    if m ? ${super.name}
+    then let
+      paths = m.${super.name};
+    in {
+      src = runCommandCC "${super.name}-patched" {
+        inherit (super) leanPath src relpath;
+      } (''
+        dir=$(dirname $relpath)
+        mkdir -p $out/$dir
+        if [ -d $src ]; then cp -r $src/. $out/$dir/; else cp $src $out/$leanPath; fi
+      '' + lib.concatMapStringsSep "\n" (p : ''
+        install -D -m 644 ${emptyFile} $out/${p}
+      '') paths);
+    }
+    else {};
+}
diff --git a/docs/user/pygments.css b/docs/user/pygments.css
new file mode 100644
index 000000000..9bdcad69c
--- /dev/null
+++ b/docs/user/pygments.css
@@ -0,0 +1,83 @@
+/* Pygments stylesheet generated by Alectryon (style=None) */
+td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
+span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
+td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
+span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
+.highlight .hll, .code .hll { background-color: #ffffcc }
+.highlight .c, .code .c { color: #555753; font-style: italic } /* Comment */
+.highlight .err, .code .err { color: #a40000; border: 1px solid #cc0000 } /* Error */
+.highlight .g, .code .g { color: #000000 } /* Generic */
+.highlight .k, .code .k { color: #8f5902 } /* Keyword */
+.highlight .l, .code .l { color: #2e3436 } /* Literal */
+.highlight .n, .code .n { color: #000000 } /* Name */
+.highlight .o, .code .o { color: #000000 } /* Operator */
+.highlight .x, .code .x { color: #2e3436 } /* Other */
+.highlight .p, .code .p { color: #000000 } /* Punctuation */
+.highlight .ch, .code .ch { color: #555753; font-weight: bold; font-style: italic } /* Comment.Hashbang */
+.highlight .cm, .code .cm { color: #555753; font-style: italic } /* Comment.Multiline */
+.highlight .cp, .code .cp { color: #3465a4; font-style: italic } /* Comment.Preproc */
+.highlight .cpf, .code .cpf { color: #555753; font-style: italic } /* Comment.PreprocFile */
+.highlight .c1, .code .c1 { color: #555753; font-style: italic } /* Comment.Single */
+.highlight .cs, .code .cs { color: #3465a4; font-weight: bold; font-style: italic } /* Comment.Special */
+.highlight .gd, .code .gd { color: #a40000 } /* Generic.Deleted */
+.highlight .ge, .code .ge { color: #000000; font-style: italic } /* Generic.Emph */
+.highlight .gr, .code .gr { color: #a40000 } /* Generic.Error */
+.highlight .gh, .code .gh { color: #a40000; font-weight: bold } /* Generic.Heading */
+.highlight .gi, .code .gi { color: #4e9a06 } /* Generic.Inserted */
+.highlight .go, .code .go { color: #000000; font-style: italic } /* Generic.Output */
+.highlight .gp, .code .gp { color: #8f5902 } /* Generic.Prompt */
+.highlight .gs, .code .gs { color: #000000; font-weight: bold } /* Generic.Strong */
+.highlight .gu, .code .gu { color: #000000; font-weight: bold } /* Generic.Subheading */
+.highlight .gt, .code .gt { color: #000000; font-style: italic } /* Generic.Traceback */
+.highlight .kc, .code .kc { color: #204a87; font-weight: bold } /* Keyword.Constant */
+.highlight .kd, .code .kd { color: #4e9a06; font-weight: bold } /* Keyword.Declaration */
+.highlight .kn, .code .kn { color: #4e9a06; font-weight: bold } /* Keyword.Namespace */
+.highlight .kp, .code .kp { color: #204a87 } /* Keyword.Pseudo */
+.highlight .kr, .code .kr { color: #8f5902 } /* Keyword.Reserved */
+.highlight .kt, .code .kt { color: #204a87 } /* Keyword.Type */
+.highlight .ld, .code .ld { color: #2e3436 } /* Literal.Date */
+.highlight .m, .code .m { color: #2e3436 } /* Literal.Number */
+.highlight .s, .code .s { color: #ad7fa8 } /* Literal.String */
+.highlight .na, .code .na { color: #c4a000 } /* Name.Attribute */
+.highlight .nb, .code .nb { color: #75507b } /* Name.Builtin */
+.highlight .nc, .code .nc { color: #204a87 } /* Name.Class */
+.highlight .no, .code .no { color: #ce5c00 } /* Name.Constant */
+.highlight .nd, .code .nd { color: #3465a4; font-weight: bold } /* Name.Decorator */
+.highlight .ni, .code .ni { color: #c4a000; text-decoration: underline } /* Name.Entity */
+.highlight .ne, .code .ne { color: #cc0000 } /* Name.Exception */
+.highlight .nf, .code .nf { color: #a40000 } /* Name.Function */
+.highlight .nl, .code .nl { color: #3465a4; font-weight: bold } /* Name.Label */
+.highlight .nn, .code .nn { color: #000000 } /* Name.Namespace */
+.highlight .nx, .code .nx { color: #000000 } /* Name.Other */
+.highlight .py, .code .py { color: #000000 } /* Name.Property */
+.highlight .nt, .code .nt { color: #a40000 } /* Name.Tag */
+.highlight .nv, .code .nv { color: #ce5c00 } /* Name.Variable */
+.highlight .ow, .code .ow { color: #8f5902 } /* Operator.Word */
+.highlight .w, .code .w { color: #d3d7cf; text-decoration: underline } /* Text.Whitespace */
+.highlight .mb, .code .mb { color: #2e3436 } /* Literal.Number.Bin */
+.highlight .mf, .code .mf { color: #2e3436 } /* Literal.Number.Float */
+.highlight .mh, .code .mh { color: #2e3436 } /* Literal.Number.Hex */
+.highlight .mi, .code .mi { color: #2e3436 } /* Literal.Number.Integer */
+.highlight .mo, .code .mo { color: #2e3436 } /* Literal.Number.Oct */
+.highlight .sa, .code .sa { color: #ad7fa8 } /* Literal.String.Affix */
+.highlight .sb, .code .sb { color: #ad7fa8 } /* Literal.String.Backtick */
+.highlight .sc, .code .sc { color: #ad7fa8; font-weight: bold } /* Literal.String.Char */
+.highlight .dl, .code .dl { color: #ad7fa8 } /* Literal.String.Delimiter */
+.highlight .sd, .code .sd { color: #ad7fa8 } /* Literal.String.Doc */
+.highlight .s2, .code .s2 { color: #ad7fa8 } /* Literal.String.Double */
+.highlight .se, .code .se { color: #ad7fa8; font-weight: bold } /* Literal.String.Escape */
+.highlight .sh, .code .sh { color: #ad7fa8; text-decoration: underline } /* Literal.String.Heredoc */
+.highlight .si, .code .si { color: #ce5c00 } /* Literal.String.Interpol */
+.highlight .sx, .code .sx { color: #ad7fa8 } /* Literal.String.Other */
+.highlight .sr, .code .sr { color: #ad7fa8 } /* Literal.String.Regex */
+.highlight .s1, .code .s1 { color: #ad7fa8 } /* Literal.String.Single */
+.highlight .ss, .code .ss { color: #8f5902 } /* Literal.String.Symbol */
+.highlight .bp, .code .bp { color: #5c35cc } /* Name.Builtin.Pseudo */
+.highlight .fm, .code .fm { color: #a40000 } /* Name.Function.Magic */
+.highlight .vc, .code .vc { color: #ce5c00 } /* Name.Variable.Class */
+.highlight .vg, .code .vg { color: #ce5c00; text-decoration: underline } /* Name.Variable.Global */
+.highlight .vi, .code .vi { color: #ce5c00 } /* Name.Variable.Instance */
+.highlight .vm, .code .vm { color: #ce5c00 } /* Name.Variable.Magic */
+.highlight .il, .code .il { color: #2e3436 } /* Literal.Number.Integer.Long */
+.hljs-doctag { color: green  }
+.hljs-comment { color: green  }
\ No newline at end of file
diff --git a/docs/user/src/SUMMARY.md b/docs/user/src/SUMMARY.md
index 54a6905b9..6741ea873 100644
--- a/docs/user/src/SUMMARY.md
+++ b/docs/user/src/SUMMARY.md
@@ -6,6 +6,5 @@
 
 # Proving with Lean
 
-## Tactics guide
-
-- [Progress](./lean/tactics/progress.md)
+- [Getting started]()
+  - [Factorial function](./lean/basics/factorial.lean.md)
diff --git a/docs/user/src/lean/basics/factorial.lean b/docs/user/src/lean/basics/factorial.lean
new file mode 100644
index 000000000..17beaf1a9
--- /dev/null
+++ b/docs/user/src/lean/basics/factorial.lean
@@ -0,0 +1,196 @@
+import Base
+import Mathlib.Data.Nat.Factorial.Basic
+
+/-!
+
+# Computing factorial
+
+Test 1, test 2, test 3.
+
+-/
+
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace factorial
+
+/- [factorial::factorial]:
+   Source: 'src/factorial.rs', lines 1:0-1:27 -/
+divergent def factorial (n : U64) : Result U64 :=
+  if n = 0#u64
+  then Result.ok 1#u64
+  else do
+       let i ← n - 1#u64
+       let i1 ← factorial i
+       n * i1
+
+end factorial
+
+/-!
+
+We will need some lemmas on factorials lifted to ℤ and U64
+to prove theorems about factorial.
+
+This will be useful to introduce arithmetic work in Aeneas.
+
+First, we would like to prove that the factorial of natural number as integers possess
+the recursive property of factorials.
+-/
+
+lemma Int.mul_factorial_pred: ∀ {n: ℤ}, 0 < n → n * (n - 1).toNat.factorial = n.toNat.factorial := by
+  intro n n_pos
+  -- This is a generic tactic to lift types to another types while discharging conditions, e.g. positivity, etc.
+  lift (n: ℤ) to ℕ
+  -- `omega` is another generic tactic to close arithmetic goals automatically, `linarith` is another option
+  -- for linear arithmetic.
+  omega
+  -- `simp` here is used as a normalization tactic, then we normalize the casts themselves
+  -- and finally, we use the natural number version of the recursive property.
+  -- `exact_mod_cast` is a "here's the term modulo casts" tactic.
+  simp; norm_cast; exact Nat.mul_factorial_pred (by exact_mod_cast n_pos)
+
+
+lemma U64.mul_factorial_pred: ∀ {n: U64}, 0#u64 < n → (n: ℤ) * (n.toNat - 1).factorial = n.toNat.factorial := by
+  intro n n_pos
+  -- `convert` is a "here's the term, please match it as much as you can and let me discharge the differences".
+  convert (Int.mul_factorial_pred _)
+  . simp
+  . scalar_tac
+
+/-!
+
+We will need a mathematical theorem relating machine integers
+as Rust cannot compute factorials larger than 2^64 - 1 using u64s.
+
+As factorial is a nice function, i.e. is increasing, we can just reduce
+the proof to proving that our domain's max value fits in a U64, i.e. 20! ≤ 2^64 - 1.
+
+In Lean, certain goals can be "decided", e.g. we can just use a fast algorithm
+to produce a proof certificate that something is true.
+-/
+theorem factorial_bounds: ∀ {n: ℕ}, n ≤ 20 → n.factorial ≤ U64.max := by
+  intro n n_pos
+  -- Our strategy will be to write this in ℕ to reuse natural number theorems.
+  rw [U64.max]
+  norm_cast
+  -- We use transitivity of ≤ to use the natural number theorem _and_ decision.
+  transitivity
+  . exact Nat.factorial_le n_pos
+  . decide
+
+/-! 
+
+We define a restricted scalar factorial to U64.
+To construct a scalar, we need to prove that it fits both of the ends of the scalar.
+For unsigned scalar, we only need to prove positivity _and_ it fits the max.
+
+We leave the problem to `scalar_tac`, an Aeneas tactic that performs pre-processing step
+and knows facts about scalars to discharge scalar-related goals. This tactic calls internally `omega`,
+so it is _at least_ powerful as `omega`.
+
+For the upper-bound, we reuse our just-proven theorem.
+-/
+def scalar_factorial {n: ℕ} (bounds: n ≤ 20): U64 :=
+  Scalar.ofIntCore n.factorial ⟨ by scalar_tac, factorial_bounds bounds ⟩
+
+/-!
+
+We are ready to create the specification of factorial.
+
+That is, under the precondition of having an integer smaller than 20, the Rust's extracted factorial function
+coincides with the theoretical scalar factorial function lifted from the mathematical scalar factorial function.
+
+Nonetheless, we will not be able to finish the formalization with the proposed signature.
+
+`@[pspec]`, a decorator, marks the following theorem as a specification, which can be searched by Aeneas tactics on specifications.
+-/
+
+@[pspec]
+theorem factorial_spec_mistaken: ∀ (n: ℕ), 
+  (bounds: n ≤ 20) → 
+  -- We cast the input natural number it in a scalar.
+  factorial.factorial (Scalar.ofIntCore n ⟨ by scalar_tac, by scalar_tac ⟩) = Result.ok (scalar_factorial bounds)  := by
+  intro n bounds
+  -- We unfold the Rust definition.
+  rw [factorial.factorial]
+  -- Distinguish the trivial case and the complicated case.
+  by_cases hzero : n = 0
+  . 
+    -- We let Lean reduce this to a trivial equation.
+    simp [hzero, scalar_factorial]
+  . 
+    -- We simplify the branching using our negation hypothesis.
+    simp [hzero]
+    /-
+      Here, we need to reuse a specification on scalar substraction regarding `n - 1`
+      `k` will be the new integer in the context and `Hk` the term that links `k`
+      to its value.
+      This specification can be discovered automatically and pasted by `progress?`.
+      `progress` is one of the Aeneas tactics on specifications.
+    -/
+    progress with Primitives.U64.sub_spec as ⟨ k, Hk ⟩
+    -- We have a problem here, the goal ask us to reuse our specification
+    -- but with a `k`, not with a `Scalar.ofIntCore ...`
+    -- rw [Hk]
+    -- progress with factorial_spec
+    stop
+
+/-!
+In general, specifications in Aeneas are written with an existential-style, that is, we will write there's a result
+to some operation and we will attach additional conditions to the value of the result.
+
+This avoids to depend on things like proofs of boundness of a given scalar which could be arbitrary.
+
+Here's a fixed proposal.
+-/
+
+@[pspec]
+theorem factorial_spec: ∀ (n: U64), (bounds: n.val ≤ 20) → ∃ v, factorial.factorial n = Result.ok v ∧ v.val = n.val.toNat.factorial := by
+  intro n bounds
+  rw [factorial.factorial]
+  by_cases hzero : n = 0#u64
+  . 
+    -- We let Lean reduce this to a trivial equation.
+    simp [hzero, scalar_factorial]
+  . 
+    -- We simplify the branching using our negation hypothesis.
+    simp [hzero]
+    -- Here, we need to reuse a specification on scalar substraction regarding `n - 1`
+    -- `k` will be the new integer in the context and `Hk` the term that links `k`
+    -- to its value.
+    -- This specification can be discovered automatically and pasted by `progress?`.
+    progress with Primitives.U64.sub_spec as ⟨ k, Hk ⟩
+    -- Here, we have the recursive call to `factorial`
+    -- Lean will figure out automatically that calling ourselves with a smaller argument
+    -- is sufficient to prove termination of this specification proof.
+    progress with factorial_spec as ⟨ p, Hp ⟩
+    -- We still need to prove that np is a valid U64 scalar
+    -- and its value is what is expected.
+    progress with Primitives.U64.mul_spec as ⟨ y, Hy ⟩
+    -- We replace our collected equalities in the previous progresses.
+    . 
+      rw [Hp, Hk]
+      -- We do various wrangling with the equalities to simplify
+      -- their casts, their form, remove the definitions (U64.max).
+      simp only [Scalar.ofInt_val_eq, Int.pred_toNat]
+      -- We leave it to Aeneas automation to discharge the non-negativity of the scalar.
+      rw [U64.mul_factorial_pred (by scalar_tac)]
+      simp only [U64.toNat]
+      -- Our original bound live in ℤ, we need it in ℕ, let's lift it quickly.
+      have bounds' : n.toNat ≤ 20 := by {
+        -- Let's lift the goal, i.e. the inequality in ℕ, to ℤ and conclude immediately.
+        zify; simp [bounds]
+      }
+      exact factorial_bounds bounds'
+    . rw [Hy, Hp, Hk]
+      simp only [Scalar.ofInt_val_eq, Int.pred_toNat]
+      rw [U64.mul_factorial_pred (by scalar_tac)]
+-- We need to prove that we are calling the specification with a smaller scalar.
+-- Let's prove it over the cast to natural numbers.
+termination_by n => n.val.toNat
+decreasing_by
+  simp_wf -- We simplify the well-founded relation definition.
+  rw [Hk] -- Inject the definition of `k`.
+  simp -- Let a Lean tactic conclude trivially.
diff --git a/docs/user/src/lean/basics/factorial.lean.md b/docs/user/src/lean/basics/factorial.lean.md
new file mode 100644
index 000000000..5b0e9048c
--- /dev/null
+++ b/docs/user/src/lean/basics/factorial.lean.md
@@ -0,0 +1,3 @@
+```lean
+{{#include factorial.lean}}
+```
diff --git a/docs/user/src/lean/bst/height.md b/docs/user/src/lean/bst/height.md
new file mode 100644
index 000000000..32daf62cb
--- /dev/null
+++ b/docs/user/src/lean/bst/height.md
@@ -0,0 +1 @@
+# Verifying Height Operation
diff --git a/docs/user/src/lean/bst/invariants.md b/docs/user/src/lean/bst/invariants.md
new file mode 100644
index 000000000..214e26f81
--- /dev/null
+++ b/docs/user/src/lean/bst/invariants.md
@@ -0,0 +1,32 @@
+# Invariants of a binary search tree
+
+The binary search tree invariant \\( \textrm{BST}(T) \\) can be defined inductively:
+
+- \\( \textrm{BST}(\emptyset) \\) where \\( \emptyset \\) is the empty binary tree
+- yadayada
+
+Mirroring this mathematical definition in the Lean theorem prover yields to an inductive predicate:
+
+```lean
+-- A helper inductive predicate over trees
+
+inductive ForallNode (p: T -> Prop): Tree T -> Prop
+| none : ForallNode p none
+| some (a: T) (left: Tree T) (right: Tree T) : ForallNode p left -> p a -> ForallNode p right -> ForallNode p (some (Node.mk a left right))
+
+--- To express inequalities between values of `T`, it is necessary to require an linear order (also known as total order) over `T`.
+variable [LinearOrder T]
+inductive Invariant: Tree T -> Prop
+| none : Invariant none
+| some (a: T) (left: Tree T) (right: Tree T) : 
+  ForallNode (fun v => v < a) left -> ForallNode (fun v => a < v) right
+  -> Invariant left -> Invariant right -> Invariant (some (Node.mk a left right))
+```
+
+Once those definitions are provided, helper theorems on `ForallNode` and `Invariant` will be useful.
+
+As exercises, consider proving the following statements:
+
+- `ForallNode.not_mem {a: T} (p: T -> Prop) (t: Option (Node T)): ¬ p a -> ForallNode p t -> a ∉ Tree.set t`: given an element \\( a \\) and a predicate \\( p \\), if \\( \lnot p(a) \\) but all the nodes in the tree \\( t \\) verifies the predicate \\( p \\), then \\( a \\) cannot be part of that tree.
+- `singleton_bst {a: T}: Invariant (some (Node.mk a none none))` : the "singleton" tree, i.e. a tree with no subtrees, is a binary search tree.
+- `left_pos {left right: Option (Node T)} {a x: T}: BST.Invariant (some (Node.mk a left right)) -> x ∈ Tree.set (Node.mk a left right) -> x < a -> x ∈ Tree.set left`, that is a sub-tree localisation theorem by comparing \\( x \\) to the root.
diff --git a/docs/user/src/lean/bst/loops.md b/docs/user/src/lean/bst/loops.md
new file mode 100644
index 000000000..dae87723d
--- /dev/null
+++ b/docs/user/src/lean/bst/loops.md
@@ -0,0 +1 @@
+# Dealing with Loops
diff --git a/docs/user/src/lean/bst/math-repr.md b/docs/user/src/lean/bst/math-repr.md
new file mode 100644
index 000000000..822303fa7
--- /dev/null
+++ b/docs/user/src/lean/bst/math-repr.md
@@ -0,0 +1,169 @@
+# Picking mathematical representations
+
+While defining binary search trees and its operations, we needed to assume that `T`, the type of elements, supported a comparison operation:
+
+```rust,noplayground
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+trait Ord {
+    fn cmp(&self, other: &Self) -> Ordering;
+}
+
+impl Ord for u32 {
+    fn cmp(&self, other: &Self) -> Ordering {
+        if *self < *other {
+            Ordering::Less
+        } else if *self == *other {
+            Ordering::Equal
+        } else {
+            Ordering::Greater
+        }
+    }
+}
+```
+
+To be able to verify that the binary search tree works the way we expect, we need two ingredients:
+
+- figure out what is the mathematical representation of the order we need for the binary search tree: in the invariant section, we chose `LinearOrder T` which is a total order over `T`. It's sufficient to build a theory of *sound* binary search trees.
+
+- ensure that actual trait implementations satisfy our mathematical refinement we need for our verification: prove that the `u32` implementation of `Ord` yields to a `LinearOrder U32` in Lean.
+
+## Why is it necessary to care about `Ord` ?
+
+Consider this implementation of `Ord` for `u32`:
+
+```rust,noplayground
+impl Ord for u32 {
+    fn cmp(&self, other: &Self) -> Ordering {
+        if *self == 5924 { panic!(); }
+        
+        if *self < *other {
+            Ordering::Less
+        } else if *self == *other {
+            Ordering::Equal
+        } else {
+            Ordering::Greater
+        }
+    }
+}
+```
+
+A `u32` tree based on that implementation will not have any issue as long as we never insert `5924` in there.
+
+From this, trait implementations have load-bearing consequences on the correctness of more complicated structures such as a tree and the verification needs to take them into account to ensure a complete correctness.
+
+Furthermore, this problem can arise if the mathematical representation chosen is too ideal: that is, no trait implementation can be written such that it fulfills the mathematical representation chosen, or, **worse**, there's no such mathematical object *at all*.
+
+If a whole verification is constructed on the top of an *impossible-to-fulfill-in-practice* mathematical representation, large changes may be necessary to repair the representation.
+
+## Scalar theory in Aeneas
+
+Aeneas provides a generic `Scalar` type mirroring some of the Rust scalar theory, i.e. scalar operations such as additions and multiplications are mirrored faithfully.
+
+In Rust, scalars does not form an ideal mathematical structure, that is: `U64` is not \(( \mathbb{N} \)).
+
+Likewise, additions of `U64` is well-defined as long as the result is contained in a `U64`, which means that the addition is fallible. 
+
+In practice, Rust will panic if addition overflows unexpectedly (i.e. the code makes no use of explicit overflowing addition operators), the extraction reflects this behavior by having most operations returns a `Result (Scalar ScalarTy)` where `ScalarTy` are the word sizes, e.g. `.U32`.
+
+Nonetheless, Rust scalars do enjoy bits of mathematical structure such as linear order definitions and panic-freedomness with their default trait implementations.
+
+## A linear order over `Scalar .U32`
+
+Here, we will give an example of a `LinearOrder` definition for the Aeneas scalars:
+
+```lean
+instance ScalarU32DecidableLE : DecidableRel (· ≤ · : U32 -> U32 -> Prop) := by
+  simp [instLEScalar]
+  -- Lift this to the decidability of the Int version.
+  infer_instance
+
+instance : LinearOrder (Scalar .U32) where
+  le_antisymm := fun a b Hab Hba => by
+    apply (Scalar.eq_equiv a b).2; exact (Int.le_antisymm ((Scalar.le_equiv _ _).1 Hab) ((Scalar.le_equiv _ _).1 Hba))
+  le_total := fun a b => by
+    rcases (Int.le_total a b) with H | H 
+    left; exact (Scalar.le_equiv _ _).2 H 
+    right; exact (Scalar.le_equiv _ _).2 H
+  decidableLE := ScalarU32DecidableLE
+```
+
+This definition just exploits the fact that Aeneas' scalars can be injected in \(( \mathbb{Z} \)) and that various properties can be transferred back'n'forth via an equivalence theorem.
+
+This definition is part of the Aeneas standard library, so you usually do not have to write your own definitions.
+
+If you find a missing generic definition that could be useful in general, do not hesitate to send a pull request to the Aeneas project.
+
+## An bundling of Rust orders in Lean world
+
+Nonetheless, the previous definition is insufficient on its own, as a user can provide its own `Ord` implementation, we need to bundle a user-provided `Ord` implementation with a verification-provided `Ord` specification.
+
+Consider the following:
+
+```lean
+variable {T: Type} (H: outParam (verification.Ord T))
+
+-- Panic-freedomness of the Rust `Ord` implementation `H`
+class OrdSpec [Ord T] where
+  infallible: ∀ a b, ∃ (o: verification.Ordering), H.cmp a b = .ok o ∧ compare a b = o.toLeanOrdering
+
+-- `a ≤ b <-> b ≥ a`
+class OrdSpecSymmetry [O: Ord T] extends OrdSpec H where
+  symmetry: ∀ a b, O.compare a b = (O.opposite.compare a b).toDualOrdering
+
+-- A generalized equality specification
+class OrdSpecRel [O: Ord T] (R: outParam (T -> T -> Prop)) extends OrdSpec H where
+  equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b
+
+-- We specialize the previous specifications to the case of the equivalence relation `=`, equality.
+class OrdSpecLinearOrderEq [O: Ord T] extends OrdSpecSymmetry H, OrdSpecRel H Eq
+```
+
+With all those pieces, we only need to prove that the extracted `OrdU32` implementation fulfills `OrdSpecLinearOrderEq` which is one of the pre-requisite to benefit from a formal verification of binary search trees over Rust `u32` scalars.
+
+Here's a solution to that proof:
+
+```lean
+instance : OrdSpecLinearOrderEq OrdU32 where
+  infallible := fun a b => by
+    unfold Ord.cmp
+    unfold OrdU32
+    unfold OrdU32.cmp
+    rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+    if hlt : a < b then 
+      use .Less
+      simp [hlt]
+    else
+      if heq: a = b
+      then
+      use .Equal
+      simp [hlt]
+      rw [heq]
+      else
+        use .Greater
+        simp [hlt, heq]
+  symmetry := fun a b => by
+    rw [Ordering.toDualOrdering, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+    rw [compare, Ord.opposite]
+    simp [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+    split_ifs with hab hba hba' hab' hba'' _ hba₃ _ <;> tauto
+    exact lt_irrefl _ (lt_trans hab hba)
+    rw [hba'] at hab; exact lt_irrefl _ hab
+    rw [hab'] at hba''; exact lt_irrefl _ hba''
+    -- The order is total, therefore, we have at least one case where we are comparing something.
+    cases (lt_trichotomy a b) <;> tauto
+  equivalence := fun a b => by
+    unfold Ord.cmp
+    unfold OrdU32
+    unfold OrdU32.cmp
+    simp only []
+    split_ifs <;> simp only [Result.ok.injEq, not_false_eq_true, neq_imp, IsEmpty.forall_iff]; tauto; try assumption
+```
+
+Proving panic-freedomness, symmetry and equality comes from definition unfolding and going through the Rust code which is equal to a 'canonical' definition of `compare` assuming the existence of an linear order.
+
+Therefore, we just reuse the linear order properties to finish most of those proofs once all definitions are unfolded.
diff --git a/docs/user/src/lean/bst/progress.md b/docs/user/src/lean/bst/progress.md
new file mode 100644
index 000000000..1785bb71d
--- /dev/null
+++ b/docs/user/src/lean/bst/progress.md
@@ -0,0 +1 @@
+# The Progress Tactic
diff --git a/docs/user/src/lean/bst/refining.md b/docs/user/src/lean/bst/refining.md
new file mode 100644
index 000000000..16aad49eb
--- /dev/null
+++ b/docs/user/src/lean/bst/refining.md
@@ -0,0 +1 @@
+# Refining the Translation
diff --git a/docs/user/src/lean/bst/scalars.md b/docs/user/src/lean/bst/scalars.md
new file mode 100644
index 000000000..8a6e9bc95
--- /dev/null
+++ b/docs/user/src/lean/bst/scalars.md
@@ -0,0 +1 @@
+# Dealing with Machine Integers: scalar_tac Tactic
diff --git a/docs/user/src/lean/bst/set_of_values.md b/docs/user/src/lean/bst/set_of_values.md
new file mode 100644
index 000000000..efd2c05ab
--- /dev/null
+++ b/docs/user/src/lean/bst/set_of_values.md
@@ -0,0 +1 @@
+# What does it mean to be in a tree?
diff --git a/docs/user/src/lean/bst/termination.md b/docs/user/src/lean/bst/termination.md
new file mode 100644
index 000000000..5f0278439
--- /dev/null
+++ b/docs/user/src/lean/bst/termination.md
@@ -0,0 +1 @@
+# Dealing with Termination Issues
diff --git a/docs/user/src/rust/bst_def.md b/docs/user/src/rust/bst_def.md
new file mode 100644
index 000000000..f7a3727fb
--- /dev/null
+++ b/docs/user/src/rust/bst_def.md
@@ -0,0 +1,118 @@
+# Defining Binary Search Trees in Rust
+
+## Pre-requisites
+
+Due to Aeneas limitations, we will not use Rust standard library for the order definitions, e.g. `Ord` / `Ordering`.
+
+We will define ours and we will also take them into account in the verification:
+
+```rust,noplayground
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+trait Ord {
+    fn cmp(&self, other: &Self) -> Ordering;
+}
+
+impl Ord for u32 {
+    fn cmp(&self, other: &Self) -> Ordering {
+        if *self < *other {
+            Ordering::Less
+        } else if *self == *other {
+            Ordering::Equal
+        } else {
+            Ordering::Greater
+        }
+    }
+}
+```
+
+We will revisit those definitions in the chapter about mathematical representations because we will need to decide what extra properties we want to impose on an `Ord` as Rust allows many degenerate implementations of an order which will not lead to a working binary search tree.
+
+## Data structure
+
+We define trees in Rust following borrow checker constraints, e.g. a `Box` indirection is required.
+
+```rust,noplayground
+struct Node<T> {
+   value: T,
+   left: Option<Box<Node<T>>,
+   right: Option<Box<Node<T>>
+}
+
+type Tree<T> = Option<Box<Node<T>>>;
+```
+
+**Note**: `Box` is erased during translation, i.e. in Lean, no details about `Box` will be available.
+
+**Note 2** : We do not ask for `T` to have `Ord`, we will put this trait bound on the functions in the next section.
+
+## Operations on trees
+
+We will define two operations for this guide:
+
+- `height`, defined by: $$\textrm{height}(t) = 1 + \textrm{max}(\textrm{height}(t.\textrm{left}), \textrm{height}(t.\textrm{right}))$$
+- `insert` which inserts an item inside the binary search tree
+
+**Note** : Due to Aeneas limitations, we sometimes have to rewrite the code in a way that will be possible to extract to Lean, those situations are documented with a comment to explain why it is necessary.
+
+## `insert`
+
+We will need to define a container for our tree to hold our root:
+
+```rust,noplayground
+struct TreeSet<T> {
+   root: Tree<T>
+}
+
+impl<T: Ord> TreeSet<T> {
+    pub fn new() -> Self {
+        Self { root: None }
+    }
+
+    pub fn insert(&mut self, value: T) -> bool {
+        let mut current_tree = &mut self.root;
+
+        while let Some(current_node) = current_tree {
+            match current_node.value.cmp(&value) {
+                Ordering::Less => current_tree = &mut current_node.right,
+                Ordering::Equal => return false,
+                Ordering::Greater => current_tree = &mut current_node.left,
+            }
+        }
+
+        *current_tree = Some(Box::new(Node {
+            value,
+            left: None,
+            right: None,
+        }));
+
+        true
+    }
+}
+```
+
+`insert` returns whether the item was already in or not and mutates in-place the tree.
+
+## `find`
+
+```rust,noplayground
+    pub fn find(&self, value: T) -> bool {
+        let mut current_tree = &self.root;
+
+        while let Some(current_node) = current_tree {
+            match current_node.value.cmp(&value) {
+                Ordering::Less => current_tree = &current_node.right,
+                Ordering::Equal => return true,
+                Ordering::Greater => current_tree = &current_node.left,
+            }
+        }
+
+        false
+    }
+```
+
+We return whether we find the item or not in the tree by browsing it using the binary search tree invariant.