ci(proofs): bisect — restore Coq job only

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: claude

.github/workflows/dogfood-proofs-ci.yml

@@ -1,6 +1,6 @@
 # SPDX-License-Identifier: MPL-2.0
 # Gates the ECHIDNA dogfood proof corpus (proofs/{coq,lean,agda}) in CI.
-# (Bisecting a startup_failure: minimal skeleton first, then restore jobs.)
+# (Bisecting a startup_failure: restoring jobs one at a time.)
 name: Dogfood Proof Corpus
 
 on:
@@ -31,5 +31,18 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
-      - name: Smoke
-        run: echo "skeleton OK"
+
+      - name: Install Coq
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
+          sudo apt-get install -y --fix-missing coq
+          coqc --version
+
+      - name: Install just
+        uses: taiki-e/install-action@e49978b799e49ff429d162b7a30601a569ab6538 # v2.81.1
+        with:
+          tool: just@1.51.0
+
+      - name: Type-check Coq corpus
+        run: just proofs-coq