Build failure for `README.Data.Fin.Substitution.UntypedLambda`

[andreasabel]

doc/README/Data/Fin/Substitution/UntypedLambda.agda:22,6-17
No module ≡-Reasoning in scope
when scope checking the declaration
  open ≡-Reasoning

The examples in doc/README do not seem to be covered by CI.
Which inevitably will mean that they bit-rot...
Maybe related to the latter point:

• Fix the mentions of defunct README modules #1380

[jamesmckinna]

Good catch, thanks!
Indeed, CI probably needs a thorough overhaul, but IIUC, it is a legacy decision (well before my time) not to (re-)check all READMEs, except those generated by GenerateEverything in doc/Everything. Maybe that should change?

[JacquesCarette]

Definitely should change - guaranteed bit-rot is not a good situation.

[gallais]

README is loaded in the stub used by the CI.
The issue is that this file is orphan: there is no import path leading to it
from the toplevel README.

[jamesmckinna]

Apologies for my inaccurate mental model @gallais of course you're right. But we aren't always good at updating README when new README.* modules get added (or taken away! #1380 )