README: Polish section on excluded middle

Author: Lysxia

README.md

@@ -72,18 +72,15 @@ in [`Basics.FunctionFacts.CartesianClosed_Fun`](./theories/Basics/FunctionFacts.
 
 ### Excluded middle and choice
 
-The theory of traces (`theories/ITrace/`)—which Dijkstra monads for ITree
-depend on (`theories/Dijkstra`)—assumes excluded middle, to decide whether an
+In the `itree-extra` library, the theory of traces (`extra/ITrace/`)—which Dijkstra monads for ITree
+depend on (`extra/Dijkstra`)—assumes excluded middle, to decide whether an
 itree diverges, and a type-theoretic axiom of choice, which provides a strong
 excluded middle in propositional contexts:
 
-```
+```coq
 Theorem classicT_inhabited : inhabited (forall T : Type, T + (T -> False)).
 ```
 
-Remark: excluded middle implies UIP, but we still consider UIP as a separate
-dependency because it's used in a more central part of the library.
-
 ### Exported: strong bisimulation is propositional equality
 
 The library exports the following axiom for convenience, though it's unlikely