diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
index 05ac750..daf2695 100644
--- a/.github/workflows/proofs.yml
+++ b/.github/workflows/proofs.yml
@@ -55,25 +55,19 @@ jobs:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
       - name: Install Agda + stdlib
         run: sudo apt-get update && sudo apt-get install -y agda agda-stdlib
-      - name: Register the standard library
-        run: |
-          mkdir -p "$HOME/.agda"
-          # Grab whatever .agda-lib the package ships (name is version-dependent),
-          # with a filesystem fallback. Dump the file list on failure for triage.
-          LIB="$(dpkg -L agda-stdlib 2>/dev/null | grep -m1 '\.agda-lib$' || true)"
-          [ -z "$LIB" ] && LIB="$(find /usr -name '*.agda-lib' 2>/dev/null | grep -m1 -i 'standard' || true)"
-          if [ -z "$LIB" ]; then
-            echo "::error::no .agda-lib found for agda-stdlib"; dpkg -L agda-stdlib | tail -60; exit 1
-          fi
-          echo "$LIB" > "$HOME/.agda/libraries"
-          echo "standard-library" > "$HOME/.agda/defaults"
-          echo "registered: $LIB"
       - name: Type-check CNO + OND (--safe --without-K)
         working-directory: proofs/agda
         run: |
           agda --version
-          agda --safe --without-K CNO.agda
-          agda --safe --without-K OND.agda
+          # The Ubuntu agda-stdlib package installs the SOURCES (no .agda-lib
+          # manifest), so add its root directly to Agda's include path via -i.
+          # Locate the root as the parent of Data/Nat.agda (version-dir robust).
+          NAT="$(dpkg -L agda-stdlib | grep -m1 '/Data/Nat\.agda$')"
+          STDLIB="${NAT%/Data/Nat.agda}"
+          echo "stdlib include path: $STDLIB"
+          [ -d "$STDLIB" ] || { echo "::error::agda-stdlib source dir not found"; dpkg -L agda-stdlib | tail -60; exit 1; }
+          agda --safe --without-K -i "$STDLIB" CNO.agda
+          agda --safe --without-K -i "$STDLIB" OND.agda
           echo "✓ Agda: CNO + OND type-check"
 
   z3: