Error upon fresh import of plutus-metatheory into Agda project

[lemmon-714]

Summary

Tried to use the UPLC agda from the metatheory and it failed at import.

Steps to reproduce the behavior

1. clone plutus repo
2. add name: Plutus to plutus-metatheory/Plutus.agda-lib
3. add absolute path to Plutus.agda-lib to agda libraries file
4. clone stand
5. add absolute path to standard-libary.agda-lib to agda libraries file
6. note that the name of the lib inside the agda-lib file is actually standard-library-2.1
7. create agda defaults file and add standard-library to it
8. create a new Agda project with the agda-lib file containing

   include: src
   depend: Plutus

9. create a new file src/HelloProof.agda containing

   
   open import Agda.Primitive
   open import Untyped.CEK

data ≡ {a} {A : Set a} (x : A) : A → Set a where refl : x ≡ x

reflexive : {A : Set} {x : A} → x ≡ x reflexive = refl

EDIT: commenting out everything but `import Untyped.CEK` didn't change the outcome.
10.  run agda on that file using vscode with the agda-mode extension

### Actual Result

(...)/plutus/plutus-metatheory/src/Utils/List.lagda.md:109,47-110,79 _i_213 ≡ _k_215 !=< List A when checking that the inferred type of an application _i_213 ≡ _k_215 matches the expected type List A

### Expected Result

`*All Done*`

### Describe the approach you would take to fix this

_No response_

### System info

OS: MacOS Sonoma
Plutus (tried multiples with identical result):
- commit @d1ef450 (latest)
- tag 1.20.0.0
- commit @ec781723

[michaelpj]

We are building against version 1.7.3 of the stdlib, so it seems unlikely that it will work with version 2.1.

[lemmon-714]

Thank you, that worked!